src/Pure/Pure.thy
changeset 23824 8ad7131dbfcf
parent 23432 cec811764a38
child 26426 ddac7ef1e991
     1.1 --- a/src/Pure/Pure.thy	Tue Jul 17 13:19:18 2007 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Jul 17 13:19:19 2007 +0200
     1.3 @@ -33,10 +33,6 @@
     1.4  locale (open) meta_term_syntax =
     1.5    fixes meta_term :: "'a => prop"  ("TERM _")
     1.6  
     1.7 -parse_translation {*
     1.8 -  [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)]
     1.9 -*}
    1.10 -
    1.11  lemmas [intro?] = termI
    1.12  
    1.13  
    1.14 @@ -45,10 +41,6 @@
    1.15  locale (open) meta_conjunction_syntax =
    1.16    fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.17  
    1.18 -parse_translation {*
    1.19 -  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    1.20 -*}
    1.21 -
    1.22  lemma all_conjunction:
    1.23    includes meta_conjunction_syntax
    1.24    shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"