Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proofs;
authorwenzelm
Fri, 11 May 2007 01:07:10 +0200
changeset 22933 338c7890c96f
parent 22932 53005f898665
child 22934 64ecb3d6790a
tuned proofs;
src/Pure/Pure.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle