--- a/src/HOL/Extraction/QuotRem.thy Tue Nov 13 10:54:40 2007 +0100
+++ b/src/HOL/Extraction/QuotRem.thy Tue Nov 13 10:55:08 2007 +0100
@@ -5,16 +5,9 @@
header {* Quotient and remainder *}
-theory QuotRem imports Main begin
+theory QuotRem imports Util begin
text {* Derivation of quotient and remainder using program extraction. *}
-lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
- apply (induct m)
- apply (case_tac n)
- apply (case_tac [3] n)
- apply (simp only: nat.simps, iprover?)+
- done
-
theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
proof (induct a)
case 0