src/Pure/Pure.thy
changeset 21625 fa8a7de5da28
parent 20627 30da2841553e
child 21627 b822c7e61701
     1.1 --- a/src/Pure/Pure.thy	Sat Dec 02 02:52:02 2006 +0100
     1.2 +++ b/src/Pure/Pure.thy	Sat Dec 02 02:52:07 2006 +0100
     1.3 @@ -26,6 +26,18 @@
     1.4  lemmas meta_allE = meta_spec [elim_format]
     1.5  
     1.6  
     1.7 +subsection {* Embedded terms *}
     1.8 +
     1.9 +locale (open) meta_term_syntax =
    1.10 +  fixes meta_term :: "'a => prop"  ("TERM _")
    1.11 +
    1.12 +parse_translation {*
    1.13 +  [("\<^fixed>meta_term", fn [t] => Logic.mk_term t)]
    1.14 +*}
    1.15 +
    1.16 +lemmas [intro?] = termI
    1.17 +
    1.18 +
    1.19  subsection {* Meta-level conjunction *}
    1.20  
    1.21  locale (open) meta_conjunction_syntax =