changeset 21625 | fa8a7de5da28 |
parent 20627 | 30da2841553e |
child 21627 | b822c7e61701 |
--- a/src/Pure/Pure.thy Sat Dec 02 02:52:02 2006 +0100 +++ b/src/Pure/Pure.thy Sat Dec 02 02:52:07 2006 +0100 @@ -26,6 +26,18 @@ lemmas meta_allE = meta_spec [elim_format] +subsection {* Embedded terms *} + +locale (open) meta_term_syntax = + fixes meta_term :: "'a => prop" ("TERM _") + +parse_translation {* + [("\<^fixed>meta_term", fn [t] => Logic.mk_term t)] +*} + +lemmas [intro?] = termI + + subsection {* Meta-level conjunction *} locale (open) meta_conjunction_syntax =