--- 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)))"