# HG changeset patch
# User nipkow
# Date 1097646013 -7200
# Node ID 9473137b35507bccfedfc94050abedb09cbf0306
# Parent  ba52fdc2c4e8076e746cb82d9ee7a27c4036fefd
mod becuase of chnage in induct

diff -r ba52fdc2c4e8 -r 9473137b3550 src/HOL/Extraction/QuotRem.thy
--- 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