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