| changeset 21627 | b822c7e61701 |
| parent 21625 | fa8a7de5da28 |
| child 22933 | 338c7890c96f |
| 21626:03fe6d36e948 | 21627:b822c7e61701 |
|---|---|
30 |
30 |
31 locale (open) meta_term_syntax = |
31 locale (open) meta_term_syntax = |
32 fixes meta_term :: "'a => prop" ("TERM _") |
32 fixes meta_term :: "'a => prop" ("TERM _") |
33 |
33 |
34 parse_translation {* |
34 parse_translation {* |
35 [("\<^fixed>meta_term", fn [t] => Logic.mk_term t)] |
35 [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)] |
36 *} |
36 *} |
37 |
37 |
38 lemmas [intro?] = termI |
38 lemmas [intro?] = termI |
39 |
39 |
40 |
40 |