src/HOL/Inductive.thy
changeset 61955 e96292f32c3c
parent 61952 546958347e05
child 63400 249fa34faba2
     1.1 --- a/src/HOL/Inductive.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -370,13 +370,11 @@
     1.4  ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
     1.5  ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
     1.6  
     1.7 -text\<open>Lambda-abstractions with pattern matching:\<close>
     1.8 -
     1.9 +text \<open>Lambda-abstractions with pattern matching:\<close>
    1.10 +syntax (ASCII)
    1.11 +  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
    1.12  syntax
    1.13 -  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
    1.14 -syntax (xsymbols)
    1.15 -  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
    1.16 -
    1.17 +  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
    1.18  parse_translation \<open>
    1.19    let
    1.20      fun fun_tr ctxt [cs] =