# HG changeset patch # User wenzelm # Date 1127217817 -7200 # Node ID c84af7f39a6bbcdde659e45ef1cd5a960acdcb9d # Parent 507e519a0dad98b7d082d1a94823a72c9cc4507a tuned theory dependencies; diff -r 507e519a0dad -r c84af7f39a6b src/HOL/Binomial.thy --- 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 diff -r 507e519a0dad -r c84af7f39a6b src/HOL/Divides.thy --- 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; diff -r 507e519a0dad -r c84af7f39a6b src/HOL/Integ/IntDiv.thy --- 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 diff -r 507e519a0dad -r c84af7f39a6b src/HOL/LOrder.thy --- 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 diff -r 507e519a0dad -r c84af7f39a6b src/HOL/PreList.thy --- 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 {* diff -r 507e519a0dad -r c84af7f39a6b src/HOL/Reconstruction.thy --- 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" diff -r 507e519a0dad -r c84af7f39a6b src/HOL/Set.thy --- 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. *} diff -r 507e519a0dad -r c84af7f39a6b src/HOL/ex/Commutative_RingEx.thy --- 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" diff -r 507e519a0dad -r c84af7f39a6b src/HOL/ex/Commutative_Ring_Complete.thy --- 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 *)