equal
deleted
inserted
replaced
49 syntax (ASCII) |
49 syntax (ASCII) |
50 "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10) |
50 "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10) |
51 |
51 |
52 syntax |
52 syntax |
53 "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10) |
53 "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10) |
|
54 |
|
55 syntax_consts |
|
56 "_Lambda" \<rightleftharpoons> Abs_cfun |
54 |
57 |
55 parse_ast_translation \<open> |
58 parse_ast_translation \<open> |
56 (* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *) |
59 (* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *) |
57 (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *) |
60 (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *) |
58 let |
61 let |