Diff of /thys/Flyspeck-Tame/ListAux.thy [096842] .. [7cfccc]  Maximize  Restore

Switch to side-by-side view

--- a/thys/Flyspeck-Tame/ListAux.thy
+++ b/thys/Flyspeck-Tame/ListAux.thy
@@ -32,7 +32,7 @@
 
 subsection {* Lists *}
 
-declare mem_iff[simp] list_all_iff[simp] list_ex_iff[simp]
+declare List.member_def[simp] list_all_iff[simp] list_ex_iff[simp]
 
 
 subsubsection{* @{text length} *}
@@ -1284,7 +1284,7 @@
 definition between :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where
  "between vs ram\<^isub>1 ram\<^isub>2 \<equiv>
      let (pre\<^isub>1, post\<^isub>1) = splitAt ram\<^isub>1 vs in
-     if ram\<^isub>2 mem post\<^isub>1
+     if ram\<^isub>2 \<in> set post\<^isub>1
      then let (pre\<^isub>2, post\<^isub>2) = splitAt ram\<^isub>2 post\<^isub>1 in pre\<^isub>2
      else let (pre\<^isub>2, post\<^isub>2) = splitAt ram\<^isub>2 pre\<^isub>1 in post\<^isub>1 @ pre\<^isub>2"
 

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks