--- a/src/Pure/Pure.thy Mon Oct 27 18:14:34 2008 +0100
+++ b/src/Pure/Pure.thy Tue Oct 28 11:03:07 2008 +0100
@@ -38,7 +38,7 @@
fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
lemma all_conjunction:
- includes meta_conjunction_syntax
+ fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
proof
assume conj: "!!x. PROP A x && PROP B x"
@@ -59,7 +59,7 @@
qed
lemma imp_conjunction:
- includes meta_conjunction_syntax
+ fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
proof
assume conj: "PROP A ==> PROP B && PROP C"
@@ -80,7 +80,7 @@
qed
lemma conjunction_imp:
- includes meta_conjunction_syntax
+ fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
proof
assume r: "PROP A && PROP B ==> PROP C"