# HG changeset patch
# User wenzelm
# Date 1178838430 -7200
# Node ID 338c7890c96f159e34b87c0e7c27bd5fbd3a43d5
# Parent  53005f89866571f746f276c716fa3000e934c032
tuned proofs;

diff -r 53005f898665 -r 338c7890c96f src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri May 11 00:43:46 2007 +0200
+++ b/src/Pure/Pure.thy	Fri May 11 01:07:10 2007 +0200
@@ -94,8 +94,11 @@
   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
 proof
   assume r: "PROP A && PROP B ==> PROP C"
-  assume "PROP A" and "PROP B"
-  show "PROP C" by (rule r) -
+  assume ab: "PROP A" "PROP B"
+  show "PROP C"
+  proof (rule r)
+    from ab show "PROP A && PROP B" .
+  qed
 next
   assume r: "PROP A ==> PROP B ==> PROP C"
   assume conj: "PROP A && PROP B"