# HG changeset patch
# User berghofe
# Date 1194947708 -3600
# Node ID e6a56be0ccaa342955d9b2d4967650f7dfb792b1
# Parent  d4f80cb18c93fc6b4140682da0e385d41bca0f70
Moved nat_eq_dec to Util.thy

diff -r d4f80cb18c93 -r e6a56be0ccaa src/HOL/Extraction/QuotRem.thy
--- 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