src/HOL/List.thy

   remdups :: "'a list => 'a list"
   remove1 :: "'a => 'a list => 'a list"
   "distinct":: "'a list => bool"
   replicate :: "nat => 'a => 'a list"
   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> (('a list) \<times> ('a list))"
   allpairs :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
-  partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> (('a list) \<times> ('a list))"
 
 abbreviation
   upto:: "nat => nat => nat list"  ("(1[_../_])") where
   "[i..j] == [i..<(Suc j)]"
 

 syntax
   -- {* list Enumeration *}
   "@list" :: "args => 'a list"    ("[(_)]")
 
   -- {* Special syntax for filter *}
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_:_./ _])")
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
 
   -- {* list update *}
   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   "" :: "lupdbind => lupdbinds"    ("_")
   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
 
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
-  "[x:xs . P]"== "filter (%x. P) xs"
+  "[x<-xs . P]"== "filter (%x. P) xs"
 
   "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "list_update xs i x"
 
 
 syntax (xsymbols)
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
 syntax (HTML output)
-  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
 
 
 text {*
   Function @{text size} is overloaded for all datatypes. Users may
   refer to the list version as @{text length}. *}

 
 nonterminals lc_qual lc_quals
 
 syntax
 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
-"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
 "_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
 "_lc_end" :: "lc_quals" ("]")
 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
 
 translations
-"[e. p\<leftarrow>xs]" => "map (%p. e) xs"
+"[e. p<-xs]" => "map (%p. e) xs"
 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
  => "concat (map (%p. _listcompr e Q Qs) xs)"
 "[e. P]" => "if P then [e] else []"
 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
  => "if P then (_listcompr e Q Qs) else []"
+
+syntax (xsymbols)
+"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+syntax (HTML output)
+"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+
 
 (*
 term "[(x,y,z). b]"
 term "[(x,y,z). x \<leftarrow> xs]"
 term "[(x,y,z). x<a, x>b]"

  apply simp
 apply simp
 done
 
 lemma sublist_shift_lemma:
-     "map fst [p:zip xs [i..<i + length xs] . snd p : A] =
-      map fst [p:zip xs [0..<length xs] . snd p + i : A]"
+     "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
+      map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
 by (induct xs rule: rev_induct) (simp_all add: add_commute)
 
 lemma sublist_append:
      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
 apply (unfold sublist_def)

 apply(induct xs) apply simp
 apply(case_tac ys)
  apply auto
 done
 
-
 subsubsection {* @{const allpairs} *}
 
 lemma allpairs_conv_concat:
  "allpairs f xs ys = concat(map (%x. map (f x) ys) xs)"
 by(induct xs) auto
 
 lemma allpairs_append:
  "allpairs f (xs @ ys) zs = allpairs f xs zs @ allpairs f ys zs"
 by(induct xs) auto
-
-
-subsubsection{*Sets of Lists*}
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
 inductive2
   listsp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"