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/HOL/HOL.thy
changeset 12023 d982f98e0f0d
parent 12003 c09427e5f554
child 12114 a8e860c86252 
--- a/src/HOL/HOL.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/HOL.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -232,7 +232,8 @@
   thus "x == y" by (rule eq_reflection)
 qed
 
-lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+lemma atomize_conj [atomize]:
+  "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
 proof
   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   show "A & B" by (rule conjI)
isabelle