mod becuase of chnage in induct
authornipkow
Wed Oct 13 07:40:13 2004 +0200 (2004-10-13)
changeset 152449473137b3550
parent 15243 ba52fdc2c4e8
child 15245 5a21d9a8f14b
mod becuase of chnage in induct
src/HOL/Extraction/QuotRem.thy
     1.1 --- a/src/HOL/Extraction/QuotRem.thy	Tue Oct 12 17:00:39 2004 +0200
     1.2 +++ b/src/HOL/Extraction/QuotRem.thy	Wed Oct 13 07:40:13 2004 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
     1.5    apply (induct m)
     1.6    apply (case_tac n)
     1.7 -  apply (case_tac [3] na)
     1.8 +  apply (case_tac [3] n)
     1.9    apply (simp only: nat.simps, rules?)+
    1.10    done
    1.11