# HG changeset patch # User haftmann # Date 1184934485 -7200 # Node ID 64b9806e160b81d13cd02cc3383556163fde7d2f # Parent 4776af8be7413236a39e20779a44b0aa0380b3f7 dropped Nat.ML legacy bindings diff -r 4776af8be741 -r 64b9806e160b src/HOL/Complex/ex/mirtac.ML --- a/src/HOL/Complex/ex/mirtac.ML Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/Complex/ex/mirtac.ML Fri Jul 20 14:28:05 2007 +0200 @@ -102,7 +102,7 @@ @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, @{thm "Suc_plus1"}] - addsimps add_ac + addsimps @{thms add_ac} addsimprocs [cancel_div_mod_proc] val simpset0 = HOL_basic_ss addsimps [mod_div_equality', Suc_plus1] diff -r 4776af8be741 -r 64b9806e160b src/HOL/HoareParallel/Mul_Gar_Coll.thy --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Jul 20 14:28:05 2007 +0200 @@ -1213,7 +1213,7 @@ --{* 47 subgoals left *} apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *}) --{* 41 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *}) +apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *}) --{* 35 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *}) --{* 31 subgoals left *} @@ -1221,7 +1221,7 @@ --{* 29 subgoals left *} apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *}) --{* 25 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *}) +apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *}) --{* 10 subgoals left *} apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+ done diff -r 4776af8be741 -r 64b9806e160b src/HOL/Nat.ML --- a/src/HOL/Nat.ML Fri Jul 20 14:28:01 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,225 +0,0 @@ -(* Title: HOL/Nat.ML - ID: $Id$ -*) - -(** legacy ML bindings **) - -structure nat = -struct - val distinct = thms "nat.distinct"; - val inject = thms "nat.inject"; - val exhaust = thm "nat.exhaust"; - val cases = thms "nat.cases"; - val split = thm "nat.split"; - val split_asm = thm "nat.split_asm"; - val induct = thm "nat.induct"; - val recs = thms "nat.recs"; - val simps = thms "nat.simps"; -end; - -val Least_Suc = thm "Least_Suc"; -val Least_Suc2 = thm "Least_Suc2"; -val One_nat_def = thm "One_nat_def"; -val Suc_Suc_eq = thm "Suc_Suc_eq"; -val Suc_def = thm "Suc_def"; -val Suc_diff_diff = thm "Suc_diff_diff"; -val Suc_diff_le = thm "Suc_diff_le"; -val Suc_inject = thm "Suc_inject"; -val Suc_leD = thm "Suc_leD"; -val Suc_leI = thm "Suc_leI"; -val Suc_le_D = thm "Suc_le_D"; -val Suc_le_eq = thm "Suc_le_eq"; -val Suc_le_lessD = thm "Suc_le_lessD"; -val Suc_le_mono = thm "Suc_le_mono"; -val Suc_lessD = thm "Suc_lessD"; -val Suc_lessE = thm "Suc_lessE"; -val Suc_lessI = thm "Suc_lessI"; -val Suc_less_SucD = thm "Suc_less_SucD"; -val Suc_less_eq = thm "Suc_less_eq"; -val Suc_mono = thm "Suc_mono"; -val Suc_mult_cancel1 = thm "Suc_mult_cancel1"; -val Suc_mult_le_cancel1 = thm "Suc_mult_le_cancel1"; -val Suc_mult_less_cancel1 = thm "Suc_mult_less_cancel1"; -val Suc_n_not_le_n = thm "Suc_n_not_le_n"; -val Suc_n_not_n = thm "Suc_n_not_n"; -val Suc_neq_Zero = thm "Suc_neq_Zero"; -val Suc_not_Zero = thm "Suc_not_Zero"; -val Suc_pred = thm "Suc_pred"; -val Zero_nat_def = thm "Zero_nat_def"; -val Zero_neq_Suc = thm "Zero_neq_Suc"; -val Zero_not_Suc = thm "Zero_not_Suc"; -val add_0 = thm "add_0"; -val add_0_right = thm "add_0_right"; -val add_Suc = thm "add_Suc"; -val add_Suc_right = thm "add_Suc_right"; -val add_ac = thms "add_ac"; -val add_assoc = thm "add_assoc"; -val add_commute = thm "add_commute"; -val add_diff_inverse = thm "add_diff_inverse"; -val add_eq_self_zero = thm "add_eq_self_zero"; -val add_gr_0 = thm "add_gr_0"; -val add_is_0 = thm "add_is_0"; -val add_is_1 = thm "add_is_1"; -val add_leD1 = thm "add_leD1"; -val add_leD2 = thm "add_leD2"; -val add_leE = thm "add_leE"; -val add_le_mono = thm "add_le_mono"; -val add_le_mono1 = thm "add_le_mono1"; -val nat_add_left_cancel = thm "nat_add_left_cancel"; -val nat_add_left_cancel_le = thm "nat_add_left_cancel_le"; -val nat_add_left_cancel_less = thm "nat_add_left_cancel_less"; -val add_left_commute = thm "add_left_commute"; -val add_lessD1 = thm "add_lessD1"; -val add_less_mono = thm "add_less_mono"; -val add_less_mono1 = thm "add_less_mono1"; -val add_mult_distrib = thm "add_mult_distrib"; -val add_mult_distrib2 = thm "add_mult_distrib2"; -val nat_add_right_cancel = thm "nat_add_right_cancel"; -val def_nat_rec_0 = thm "def_nat_rec_0"; -val def_nat_rec_Suc = thm "def_nat_rec_Suc"; -val diff_0 = thm "diff_0"; -val diff_0_eq_0 = thm "diff_0_eq_0"; -val diff_Suc = thm "diff_Suc"; -val diff_Suc_Suc = thm "diff_Suc_Suc"; -val diff_Suc_less = thm "diff_Suc_less"; -val diff_add_0 = thm "diff_add_0"; -val diff_add_assoc = thm "diff_add_assoc"; -val diff_add_assoc2 = thm "diff_add_assoc2"; -val diff_add_inverse = thm "diff_add_inverse"; -val diff_add_inverse2 = thm "diff_add_inverse2"; -val diff_cancel = thm "diff_cancel"; -val diff_cancel2 = thm "diff_cancel2"; -val diff_commute = thm "diff_commute"; -val diff_diff_left = thm "diff_diff_left"; -val diff_induct = thm "diff_induct"; -val diff_is_0_eq = thm "diff_is_0_eq"; -val diff_le_self = thm "diff_le_self"; -val diff_less_Suc = thm "diff_less_Suc"; -val diff_mult_distrib = thm "diff_mult_distrib"; -val diff_mult_distrib2 = thm "diff_mult_distrib2"; -val diff_self_eq_0 = thm "diff_self_eq_0"; -val eq_imp_le = thm "eq_imp_le"; -val gr0I = thm "gr0I"; -val gr0_conv_Suc = thm "gr0_conv_Suc"; -val gr_implies_not0 = thm "gr_implies_not0"; -val inj_Suc = thm "inj_Suc"; -val le0 = thm "le0"; -val le_0_eq = thm "le_0_eq"; -val le_SucE = thm "le_SucE"; -val le_SucI = thm "le_SucI"; -val le_Suc_eq = thm "le_Suc_eq"; -val le_add1 = thm "le_add1"; -val le_add2 = thm "le_add2"; -val le_add_diff_inverse = thm "le_add_diff_inverse"; -val le_add_diff_inverse2 = thm "le_add_diff_inverse2"; -val le_anti_sym = thm "le_anti_sym"; -val le_def = thm "le_def"; -val le_eq_less_or_eq = thm "le_eq_less_or_eq"; -val le_imp_diff_is_add = thm "le_imp_diff_is_add"; -val le_imp_less_Suc = thm "le_imp_less_Suc"; -val le_imp_less_or_eq = thm "le_imp_less_or_eq"; -val le_less_trans = thm "le_less_trans"; -val le_neq_implies_less = thm "le_neq_implies_less"; -val le_refl = thm "le_refl"; -val le_simps = thms "le_simps"; -val le_trans = thm "le_trans"; -val lessE = thm "lessE"; -val lessI = thm "lessI"; -val less_Suc0 = thm "less_Suc0"; -val less_SucE = thm "less_SucE"; -val less_SucI = thm "less_SucI"; -val less_Suc_eq = thm "less_Suc_eq"; -val less_Suc_eq_0_disj = thm "less_Suc_eq_0_disj"; -val less_Suc_eq_le = thm "less_Suc_eq_le"; -val less_add_Suc1 = thm "less_add_Suc1"; -val less_add_Suc2 = thm "less_add_Suc2"; -val less_add_eq_less = thm "less_add_eq_less"; -val less_asym = thm "less_asym"; -val less_def = thm "less_def"; -val less_eq = thm "less_eq"; -val less_iff_Suc_add = thm "less_iff_Suc_add"; -val less_imp_Suc_add = thm "less_imp_Suc_add"; -val less_imp_add_positive = thm "less_imp_add_positive"; -val less_imp_diff_less = thm "less_imp_diff_less"; -val less_imp_le = thm "less_imp_le"; -val less_irrefl = thm "less_irrefl"; -val less_le_trans = thm "less_le_trans"; -val less_linear = thm "less_linear"; -val less_mono_imp_le_mono = thm "less_mono_imp_le_mono"; -val less_not_refl = thm "less_not_refl"; -val less_not_refl2 = thm "less_not_refl2"; -val less_not_refl3 = thm "less_not_refl3"; -val less_not_sym = thm "less_not_sym"; -val less_one = thm "less_one"; -val less_or_eq_imp_le = thm "less_or_eq_imp_le"; -val less_trans = thm "less_trans"; -val less_trans_Suc = thm "less_trans_Suc"; -val less_zeroE = thm "less_zeroE"; -val max_0L = thm "max_0L"; -val max_0R = thm "max_0R"; -val max_Suc_Suc = thm "max_Suc_Suc"; -val min_0L = thm "min_0L"; -val min_0R = thm "min_0R"; -val min_Suc_Suc = thm "min_Suc_Suc"; -val mult_0 = thm "mult_0"; -val mult_0_right = thm "mult_0_right"; -val mult_1 = thm "mult_1"; -val mult_1_right = thm "mult_1_right"; -val mult_Suc = thm "mult_Suc"; -val mult_Suc_right = thm "mult_Suc_right"; -val mult_ac = thms "mult_ac"; -val mult_assoc = thm "mult_assoc"; -val mult_cancel1 = thm "mult_cancel1"; -val mult_cancel2 = thm "mult_cancel2"; -val mult_commute = thm "mult_commute"; -val mult_eq_1_iff = thm "mult_eq_1_iff"; -val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10"; -val mult_is_0 = thm "mult_is_0"; -val mult_le_cancel1 = thm "mult_le_cancel1"; -val mult_le_cancel2 = thm "mult_le_cancel2"; -val mult_le_mono = thm "mult_le_mono"; -val mult_le_mono1 = thm "mult_le_mono1"; -val mult_le_mono2 = thm "mult_le_mono2"; -val mult_left_commute = thm "mult_left_commute"; -val mult_less_cancel1 = thm "mult_less_cancel1"; -val mult_less_cancel2 = thm "mult_less_cancel2"; -val mult_less_mono1 = thm "mult_less_mono1"; -val mult_less_mono2 = thm "mult_less_mono2"; -val n_not_Suc_n = thm "n_not_Suc_n"; -val nat_distrib = thms "nat_distrib"; -val nat_induct = thm "nat_induct"; -val nat_induct2 = thm "nat_induct2"; -val nat_le_linear = thm "nat_le_linear"; -val nat_less_cases = thm "nat_less_cases"; -val nat_less_induct = thm "nat_less_induct"; -val nat_less_le = thm "nat_less_le"; -val nat_neq_iff = thm "nat_neq_iff"; -val nat_not_singleton = thm "nat_not_singleton"; -val neq0_conv = thm "neq0_conv"; -val not0_implies_Suc = thm "not0_implies_Suc"; -val not_add_less1 = thm "not_add_less1"; -val not_add_less2 = thm "not_add_less2"; -val not_gr0 = thm "not_gr0"; -val not_leE = thm "not_leE"; -val not_less0 = thm "not_less0"; -val not_less_eq = thm "not_less_eq"; -val not_less_less_Suc_eq = thm "not_less_less_Suc_eq"; -val not_less_simps = thms "not_less_simps"; -val one_eq_mult_iff = thm "one_eq_mult_iff"; -val one_is_add = thm "one_is_add"; -val one_le_mult_iff = thm "one_le_mult_iff"; -val one_reorient = thm "one_reorient"; -val pred_nat_def = thm "pred_nat_def"; -val trans_le_add1 = thm "trans_le_add1"; -val trans_le_add2 = thm "trans_le_add2"; -val trans_less_add1 = thm "trans_less_add1"; -val trans_less_add2 = thm "trans_less_add2"; -val wf_less = thm "wf_less"; -val wf_pred_nat = thm "wf_pred_nat"; -val zero_induct = thm "zero_induct"; -val zero_induct_lemma = thm "zero_induct_lemma"; -val zero_less_Suc = thm "zero_less_Suc"; -val zero_less_diff = thm "zero_less_diff"; -val zero_less_mult_iff = thm "zero_less_mult_iff"; -val zero_reorient = thm "zero_reorient"; -val linorder_neqE_nat = thm "linorder_neqE_nat"; diff -r 4776af8be741 -r 64b9806e160b src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri Jul 20 14:28:05 2007 +0200 @@ -39,7 +39,7 @@ (Simplifier.rewrite (HOL_basic_ss addsimps arith_simps @ natarith @ rel_simps - @ [if_False, if_True, add_0, add_Suc, add_number_of_left, Suc_eq_add_numeral_1] + @ [if_False, if_True, @{thm add_0}, @{thm add_Suc}, add_number_of_left, Suc_eq_add_numeral_1] @ map (fn th => th RS sym) numerals)); val nat_mul_conv = nat_add_conv; @@ -590,7 +590,7 @@ val nat_arith = @{thms "nat_arith"}; val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps) - addsimps [Let_def, if_False, if_True, add_0, add_Suc]; + addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}]; fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS; fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, idom}, diff -r 4776af8be741 -r 64b9806e160b src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri Jul 20 14:28:05 2007 +0200 @@ -115,7 +115,7 @@ @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, @{thm "Suc_plus1"}] - @ add_ac + @ @{thms add_ac} addsimprocs [cancel_div_mod_proc] val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, diff -r 4776af8be741 -r 64b9806e160b src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/Tools/TFL/post.ML Fri Jul 20 14:28:05 2007 +0200 @@ -69,7 +69,7 @@ {wf_tac = REPEAT (ares_tac wfs 1), terminator = asm_simp_tac ss 1 THEN TRY (silent_arith_tac 1 ORELSE - fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), + fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1), simplifier = Rules.simpl_conv ss []}; diff -r 4776af8be741 -r 64b9806e160b src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_core.ML Fri Jul 20 14:28:05 2007 +0200 @@ -93,19 +93,19 @@ (* Theory dependencies. *) -val Pair_inject = thm "Product_Type.Pair_inject"; +val Pair_inject = @{thm Product_Type.Pair_inject}; -val acc_induct_rule = thm "Accessible_Part.accp_induct_rule" +val acc_induct_rule = @{thm Accessible_Part.accp_induct_rule}; -val ex1_implies_ex = thm "FunDef.fundef_ex1_existence" -val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness" -val ex1_implies_iff = thm "FunDef.fundef_ex1_iff" +val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}; +val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}; +val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}; -val acc_downward = thm "Accessible_Part.accp_downward" -val accI = thm "Accessible_Part.accp.accI" -val case_split = thm "HOL.case_split_thm" -val fundef_default_value = thm "FunDef.fundef_default_value" -val not_acc_down = thm "Accessible_Part.not_accp_down" +val acc_downward = @{thm Accessible_Part.accp_downward}; +val accI = @{thm Accessible_Part.accp.accI}; +val case_split = @{thm HOL.case_split_thm}; +val fundef_default_value = @{thm FunDef.fundef_default_value}; +val not_acc_down = @{thm Accessible_Part.not_accp_down}; @@ -573,8 +573,7 @@ (** Induction rule **) -val acc_subset_induct = thm "Fun.predicate1I" RS - thm "Accessible_Part.accp_subset_induct" +val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct} fun mk_partial_induct_rule thy globals R complete_thm clauses = let @@ -704,9 +703,9 @@ (** Termination rule **) -val wf_induct_rule = thm "Wellfounded_Recursion.wfP_induct_rule"; -val wf_in_rel = thm "FunDef.wf_in_rel"; -val in_rel_def = thm "FunDef.in_rel_def"; +val wf_induct_rule = @{thm Wellfounded_Recursion.wfP_induct_rule}; +val wf_in_rel = @{thm FunDef.wf_in_rel}; +val in_rel_def = @{thm FunDef.in_rel_def}; fun mk_nest_term_case thy globals R' ihyp clause = let diff -r 4776af8be741 -r 64b9806e160b src/HOL/W0/W0.thy --- a/src/HOL/W0/W0.thy Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/W0/W0.thy Fri Jul 20 14:28:05 2007 +0200 @@ -210,7 +210,7 @@ apply (unfold free_tv_subst cod_def dom_def) apply (tactic "safe_tac set_cs") apply (cut_tac m = m and n = n in less_linear) - apply (tactic "fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1") + apply (tactic "fast_tac (HOL_cs addSIs [@{thm less_or_eq_imp_le}]) 1") apply (cut_tac m = ma and n = n in less_linear) apply (fast intro!: less_or_eq_imp_le) done @@ -618,7 +618,7 @@ apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD", thm "free_tv_subst_var" RS subsetD, thm "free_tv_app_subst_te" RS subsetD, - thm "free_tv_app_subst_tel" RS subsetD, less_le_trans, subsetD] + thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD] addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *}) -- {* builtin arithmetic in simpset messes things up *} done @@ -809,13 +809,13 @@ apply (erule impE) prefer 2 apply (fastsimp simp add: new_tv_subst) apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp, - thm "new_tv_subst_le", less_imp_le, lessI]) 1 *}) + thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *}) apply (intro strip) apply (erule allE)+ apply (erule impE) prefer 2 apply (fastsimp simp add: new_tv_subst) apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp, - thm "new_tv_subst_le", less_imp_le, lessI]) 1 *}) + thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *}) txt {* case @{text "App e1 e2"} *} apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *}) apply (intro strip) @@ -891,7 +891,7 @@ apply (intro strip) apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)") apply (tactic {* asm_simp_tac (HOL_ss addsimps - [thm "new_tv_Suc_list", lessI RS less_imp_le RS thm "new_tv_subst_le"]) 1 *}) + [thm "new_tv_Suc_list", @{thm lessI} RS @{thm less_imp_le} RS thm "new_tv_subst_le"]) 1 *}) apply (erule conjE) apply (drule new_tv_not_free_tv [THEN not_free_impl_id]) apply (simp (no_asm_simp)) diff -r 4776af8be741 -r 64b9806e160b src/HOL/ex/coopertac.ML --- a/src/HOL/ex/coopertac.ML Fri Jul 20 14:28:01 2007 +0200 +++ b/src/HOL/ex/coopertac.ML Fri Jul 20 14:28:05 2007 +0200 @@ -83,7 +83,7 @@ @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, Suc_plus1] - addsimps add_ac + addsimps @{thms add_ac} addsimprocs [cancel_div_mod_proc] val simpset0 = HOL_basic_ss addsimps [mod_div_equality', Suc_plus1]