src/HOL/Inductive.thy
changeset 23389 aaca6a8e5414
parent 22886 cdff6ef76009
child 23526 936dc616a7fb
--- a/src/HOL/Inductive.thy	Thu Jun 14 18:33:29 2007 +0200
+++ b/src/HOL/Inductive.thy	Thu Jun 14 18:33:31 2007 +0200
@@ -89,7 +89,7 @@
   then show P ..
 next
   assume "\<And>P\<Colon>bool. P"
-  then show False ..
+  then show False .
 qed
 
 lemma not_eq_False: