src/HOL/List.thy
changeset 61955 e96292f32c3c
parent 61941 31f2105521ee
child 62065 1546a042e87b
     1.1 --- a/src/HOL/List.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -77,13 +77,13 @@
     1.4  "filter P [] = []" |
     1.5  "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
     1.6  
     1.7 +text \<open>Special syntax for filter:\<close>
     1.8 +syntax (ASCII)
     1.9 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_<-_./ _])")
    1.10  syntax
    1.11 -  \<comment> \<open>Special syntax for filter\<close>
    1.12 -  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
    1.13 -syntax (xsymbols)
    1.14 -  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    1.15 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_\<leftarrow>_ ./ _])")
    1.16  translations
    1.17 -  "[x<-xs . P]"== "CONST filter (%x. P) xs"
    1.18 +  "[x<-xs . P]" \<rightleftharpoons> "CONST filter (\<lambda>x. P) xs"
    1.19  
    1.20  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.21  fold_Nil:  "fold f [] = id" |
    1.22 @@ -395,13 +395,16 @@
    1.23  
    1.24  syntax
    1.25    "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
    1.26 -  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
    1.27 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
    1.28    "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
    1.29    (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
    1.30    "_lc_end" :: "lc_quals" ("]")
    1.31    "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
    1.32    "_lc_abs" :: "'a => 'b list => 'b list"
    1.33  
    1.34 +syntax (ASCII)
    1.35 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
    1.36 +
    1.37  (* These are easier than ML code but cannot express the optimized
    1.38     translation of [e. p<-xs]
    1.39  translations
    1.40 @@ -415,9 +418,6 @@
    1.41     => "_Let b (_listcompr e Q Qs)"
    1.42  *)
    1.43  
    1.44 -syntax (xsymbols)
    1.45 -  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
    1.46 -
    1.47  parse_translation \<open>
    1.48    let
    1.49      val NilC = Syntax.const @{const_syntax Nil};