Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Pure.thy
changeset 50603 3e3c2af5e8a5
parent 50128 599c935aac82
child 51224 c3e99efacb67 
--- a/src/Pure/Pure.thy	Wed Dec 19 16:41:55 2012 +0100
+++ b/src/Pure/Pure.thy	Wed Dec 19 22:26:26 2012 +0100
@@ -146,7 +146,7 @@
 qed
 
 lemma imp_conjunction:
-  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
+  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
 proof
   assume conj: "PROP A ==> PROP B &&& PROP C"
   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
isabelle