Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mod becuase of chnage in induct
authornipkow
Wed, 13 Oct 2004 07:40:13 +0200
changeset 15244 9473137b3550
parent 15243 ba52fdc2c4e8
child 15245 5a21d9a8f14b
mod becuase of chnage in induct
src/HOL/Extraction/QuotRem.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction/QuotRem.thy	Tue Oct 12 17:00:39 2004 +0200
+++ b/src/HOL/Extraction/QuotRem.thy	Wed Oct 13 07:40:13 2004 +0200
@@ -12,7 +12,7 @@
 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
   apply (induct m)
   apply (case_tac n)
-  apply (case_tac [3] na)
+  apply (case_tac [3] n)
   apply (simp only: nat.simps, rules?)+
   done
isabelle