# HG changeset patch
# User wenzelm
# Date 1138559023 -3600
# Node ID 3a1e4ee72075c04c472a35aba884c9507bd3e797
# Parent  8e080d0252c5ab1718fcda43608a493b890cf592
tuned proofs;

diff -r 8e080d0252c5 -r 3a1e4ee72075 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Jan 29 19:23:42 2006 +0100
+++ b/src/Pure/Pure.thy	Sun Jan 29 19:23:43 2006 +0100
@@ -73,7 +73,8 @@
 lemma imp_conjunction [unfolded prop_def]:
   includes meta_conjunction_syntax
   shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
-proof (unfold prop_def, rule)
+  unfolding prop_def
+proof
   assume conj: "PROP A ==> PROP B && PROP C"
   fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
   show "PROP X"
@@ -121,6 +122,6 @@
 lemma conjunction_assoc:
   includes meta_conjunction_syntax
   shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
-  by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp)
+  unfolding conjunction_imp .
 
 end