--- a/src/HOL/Binomial.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/Binomial.thy Tue Sep 20 14:03:37 2005 +0200
@@ -2,13 +2,12 @@
ID: $Id$
Author: Lawrence C Paulson
Copyright 1997 University of Cambridge
-
*)
header{*Binomial Coefficients*}
theory Binomial
-imports SetInterval
+imports GCD
begin
text{*This development is based on the work of Andy Gordon and
@@ -24,7 +23,7 @@
(if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
lemma binomial_n_0 [simp]: "(n choose 0) = 1"
-by (case_tac "n", simp_all)
+by (cases n) simp_all
lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
by simp
@@ -188,21 +187,4 @@
finally show ?case by simp
qed
-ML
-{*
-val binomial_n_0 = thm"binomial_n_0";
-val binomial_0_Suc = thm"binomial_0_Suc";
-val binomial_Suc_Suc = thm"binomial_Suc_Suc";
-val binomial_eq_0 = thm"binomial_eq_0";
-val binomial_n_n = thm"binomial_n_n";
-val binomial_Suc_n = thm"binomial_Suc_n";
-val binomial_1 = thm"binomial_1";
-val zero_less_binomial = thm"zero_less_binomial";
-val binomial_eq_0_iff = thm"binomial_eq_0_iff";
-val zero_less_binomial_iff = thm"zero_less_binomial_iff";
-val Suc_times_binomial_eq = thm"Suc_times_binomial_eq";
-val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times";
-val times_binomial_minus1_eq = thm"times_binomial_minus1_eq";
-*}
-
end
--- a/src/HOL/Divides.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/Divides.thy Tue Sep 20 14:03:37 2005 +0200
@@ -7,7 +7,7 @@
*)
theory Divides
-imports NatArith
+imports Datatype
begin
(*We use the same class for div and mod;
--- a/src/HOL/Integ/IntDiv.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/Integ/IntDiv.thy Tue Sep 20 14:03:37 2005 +0200
@@ -9,7 +9,7 @@
header{*The Division Operators div and mod; the Divides Relation dvd*}
theory IntDiv
-imports IntArith Recdef
+imports SetInterval Recdef
uses ("IntDiv_setup.ML")
begin
--- a/src/HOL/LOrder.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/LOrder.thy Tue Sep 20 14:03:37 2005 +0200
@@ -285,48 +285,4 @@
from b c show ?thesis by (simp add: meet_imp_le)
qed
-ML {*
-val is_meet_unique = thm "is_meet_unique";
-val is_join_unique = thm "is_join_unique";
-val join_exists = thm "join_exists";
-val meet_exists = thm "meet_exists";
-val is_meet_meet = thm "is_meet_meet";
-val meet_unique = thm "meet_unique";
-val is_join_join = thm "is_join_join";
-val join_unique = thm "join_unique";
-val meet_left_le = thm "meet_left_le";
-val meet_right_le = thm "meet_right_le";
-val meet_imp_le = thm "meet_imp_le";
-val join_left_le = thm "join_left_le";
-val join_right_le = thm "join_right_le";
-val join_imp_le = thm "join_imp_le";
-val meet_join_le = thms "meet_join_le";
-val is_meet_min = thm "is_meet_min";
-val is_join_max = thm "is_join_max";
-val meet_min = thm "meet_min";
-val join_max = thm "join_max";
-val meet_idempotent = thm "meet_idempotent";
-val join_idempotent = thm "join_idempotent";
-val meet_comm = thm "meet_comm";
-val join_comm = thm "join_comm";
-val meet_assoc = thm "meet_assoc";
-val join_assoc = thm "join_assoc";
-val meet_left_comm = thm "meet_left_comm";
-val meet_left_idempotent = thm "meet_left_idempotent";
-val join_left_comm = thm "join_left_comm";
-val join_left_idempotent = thm "join_left_idempotent";
-val meet_aci = thms "meet_aci";
-val join_aci = thms "join_aci";
-val le_def_meet = thm "le_def_meet";
-val le_def_join = thm "le_def_join";
-val meet_join_absorp = thm "meet_join_absorp";
-val join_meet_absorp = thm "join_meet_absorp";
-val meet_mono = thm "meet_mono";
-val join_mono = thm "join_mono";
-val distrib_join_le = thm "distrib_join_le";
-val distrib_meet_le = thm "distrib_meet_le";
-val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";
-val modular_le = thm "modular_le";
-*}
-
end
--- a/src/HOL/PreList.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/PreList.thy Tue Sep 20 14:03:37 2005 +0200
@@ -7,7 +7,7 @@
header{*A Basis for Building the Theory of Lists*}
theory PreList
-imports Wellfounded_Relations Presburger Relation_Power GCD
+imports Wellfounded_Relations Presburger Relation_Power Binomial
begin
text {*
--- a/src/HOL/Reconstruction.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/Reconstruction.thy Tue Sep 20 14:03:37 2005 +0200
@@ -7,7 +7,7 @@
header{* Reconstructing external resolution proofs *}
theory Reconstruction
-imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction
+imports Hilbert_Choice Map Infinite_Set Extraction
uses "Tools/res_lib.ML"
"Tools/res_clause.ML"
--- a/src/HOL/Set.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/Set.thy Tue Sep 20 14:03:37 2005 +0200
@@ -6,7 +6,7 @@
header {* Set theory for higher-order logic *}
theory Set
-imports Orderings
+imports LOrder
begin
text {* A set in HOL is simply a predicate. *}
--- a/src/HOL/ex/Commutative_RingEx.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/ex/Commutative_RingEx.thy Tue Sep 20 14:03:37 2005 +0200
@@ -5,7 +5,7 @@
header {* Some examples demonstrating the comm-ring method *}
theory Commutative_RingEx
-imports Main
+imports Commutative_Ring
begin
lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
--- a/src/HOL/ex/Commutative_Ring_Complete.thy Tue Sep 20 13:58:58 2005 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy Tue Sep 20 14:03:37 2005 +0200
@@ -9,7 +9,7 @@
header {* Proof of the relative completeness of method comm-ring *}
theory Commutative_Ring_Complete
-imports Commutative_Ring (*do not use Main here, since it hides our consts*)
+imports Commutative_Ring
begin
(* Fromalization of normal form *)