equal
deleted
inserted
replaced
427 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") |
427 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") |
428 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") |
428 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") |
429 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*) |
429 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*) |
430 "_lc_end" :: "lc_quals" ("]") |
430 "_lc_end" :: "lc_quals" ("]") |
431 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") |
431 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") |
432 "_lc_abs" :: "'a => 'b list => 'b list" |
|
433 |
432 |
434 syntax (ASCII) |
433 syntax (ASCII) |
435 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _") |
434 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _") |
436 |
435 |
437 (* These are easier than ML code but cannot express the optimized |
436 (* These are easier than ML code but cannot express the optimized |