# 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: "\n::nat. m = n \ m \ 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