src/Pure/Pure.thy
changeset 23824 8ad7131dbfcf
parent 23432 cec811764a38
child 26426 ddac7ef1e991
--- a/src/Pure/Pure.thy	Tue Jul 17 13:19:18 2007 +0200
+++ b/src/Pure/Pure.thy	Tue Jul 17 13:19:19 2007 +0200
@@ -33,10 +33,6 @@
 locale (open) meta_term_syntax =
   fixes meta_term :: "'a => prop"  ("TERM _")
 
-parse_translation {*
-  [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)]
-*}
-
 lemmas [intro?] = termI
 
 
@@ -45,10 +41,6 @@
 locale (open) meta_conjunction_syntax =
   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
 
-parse_translation {*
-  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
-*}
-
 lemma all_conjunction:
   includes meta_conjunction_syntax
   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"