src/HOL/Induct/SList.thy
changeset 23281 e26ec695c9b3
parent 23235 eb365b39b36d
child 23746 a455e69c31cc
--- a/src/HOL/Induct/SList.thy	Wed Jun 06 19:12:40 2007 +0200
+++ b/src/HOL/Induct/SList.thy	Wed Jun 06 19:12:59 2007 +0200
@@ -231,14 +231,14 @@
 
 
 no_translations
-  "[x:xs . P]" == "filter (%x. P) xs"
+  "[x\<leftarrow>xs . P]" == "filter (%x. P) xs"
 
 syntax
   (* Special syntax for list_all and filter *)
   "@Alls"       :: "[idt, 'a list, bool] => bool"        ("(2Alls _:_./ _)" 10)
 
 translations
-  "[x:xs. P]" == "CONST filter(%x. P) xs"
+  "[x\<leftarrow>xs. P]" == "CONST filter(%x. P) xs"
   "Alls x:xs. P" == "CONST list_all(%x. P)xs"
 
 
@@ -540,7 +540,7 @@
 lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
 by (induct_tac "xs" rule: list_induct, simp_all)
 
-lemma mem_filter [simp]: "x mem [x:xs. P x ] = (x mem xs & P(x))"
+lemma mem_filter [simp]: "x mem [x\<leftarrow>xs. P x ] = (x mem xs & P(x))"
 by (induct_tac "xs" rule: list_induct, simp_all)
 
 (** list_all **)