src/HOL/Library/Nat_Infinity.thy
changeset 27823 52971512d1a2
parent 27487 c8a6ce181805
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sun Aug 10 12:38:26 2008 +0200
     1.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Aug 11 14:49:53 2008 +0200
     1.3 @@ -317,13 +317,9 @@
     1.4  
     1.5  instance inat :: wellorder
     1.6  proof
     1.7 -  show "wf {(x::inat, y::inat). x < y}"
     1.8 -  proof (rule wfUNIVI)
     1.9 -    fix P and x :: inat
    1.10 -    assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
    1.11 -    hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
    1.12 -    thus "P x" by (rule inat_less_induct)
    1.13 -  qed
    1.14 +  fix P and n
    1.15 +  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
    1.16 +  show "P n" by (blast intro: inat_less_induct hyp)
    1.17  qed
    1.18  
    1.19