dropped legacy ML bindings
authorhaftmann
Thu Mar 29 14:21:45 2007 +0200 (2007-03-29)
changeset 225486ce4bddf3bcb
parent 22547 c3290f4382e4
child 22549 ab23925c64d6
dropped legacy ML bindings
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Integ/presburger.ML
src/HOL/Lattices.thy
src/HOL/OrderedGroup.thy
src/HOL/Orderings.thy
src/HOL/Real/ferrante_rackoff.ML
src/HOL/Real/ferrante_rackoff_proof.ML
src/HOL/Real/rat_arith.ML
src/HOL/Ring_and_Field.thy
src/HOL/Tools/Presburger/presburger.ML
src/HOL/W0/W0.thy
src/HOL/arith_data.ML
src/HOL/ex/MT.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Mar 29 11:59:54 2007 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Mar 29 14:21:45 2007 +0200
     1.3 @@ -280,19 +280,19 @@
     1.4                     pred_1, pred_0, pred_Pls, pred_Min];
     1.5  
     1.6  (*To let us treat subtraction as addition*)
     1.7 -val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
     1.8 +val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
     1.9  
    1.10  (*push the unary minus down: - x * y = x * - y *)
    1.11  val minus_mult_eq_1_to_2 =
    1.12 -    [minus_mult_left RS sym, minus_mult_right] MRS trans |> standard;
    1.13 +    [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
    1.14  
    1.15  (*to extract again any uncancelled minuses*)
    1.16  val minus_from_mult_simps =
    1.17 -    [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
    1.18 +    [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
    1.19  
    1.20  (*combine unary minus with numeric literals, however nested within a product*)
    1.21  val mult_minus_simps =
    1.22 -    [mult_assoc, minus_mult_left, minus_mult_eq_1_to_2];
    1.23 +    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
    1.24  
    1.25  (*Apply the given rewrite (if present) just once*)
    1.26  fun trans_tac NONE      = all_tac
    1.27 @@ -495,26 +495,26 @@
    1.28  (* reduce contradictory <= to False *)
    1.29  val add_rules =
    1.30      simp_thms @ arith_simps @ rel_simps @ arith_special @
    1.31 -    [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
    1.32 -     minus_zero, diff_minus, left_minus, right_minus,
    1.33 -     mult_zero_left, mult_zero_right, mult_num1, mult_1_right,
    1.34 -     minus_mult_left RS sym, minus_mult_right RS sym,
    1.35 -     minus_add_distrib, minus_minus, mult_assoc,
    1.36 +    [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
    1.37 +     @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
    1.38 +     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
    1.39 +     @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
    1.40 +     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
    1.41       of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
    1.42       of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]
    1.43  
    1.44 -val nat_inj_thms = [zle_int RS iffD2,
    1.45 -                    int_int_eq RS iffD2]
    1.46 +val nat_inj_thms = [zle_int RS iffD2, int_int_eq RS iffD2]
    1.47  
    1.48 -val Int_Numeral_Base_Simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
    1.49 -               Int_Numeral_Simprocs.cancel_numerals
    1.50 +val Int_Numeral_Base_Simprocs = assoc_fold_simproc
    1.51 +  :: Int_Numeral_Simprocs.combine_numerals
    1.52 +  :: Int_Numeral_Simprocs.cancel_numerals;
    1.53  
    1.54  in
    1.55  
    1.56  val int_arith_setup =
    1.57    Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.58     {add_mono_thms = add_mono_thms,
    1.59 -    mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
    1.60 +    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
    1.61      inj_thms = nat_inj_thms @ inj_thms,
    1.62      lessD = lessD @ [zless_imp_add1_zle],
    1.63      neqE = neqE,
    1.64 @@ -528,45 +528,10 @@
    1.65  end;
    1.66  
    1.67  val fast_int_arith_simproc =
    1.68 -  Simplifier.simproc (Theory.sign_of (the_context()))
    1.69 +  Simplifier.simproc @{theory}
    1.70    "fast_int_arith" 
    1.71       ["(m::'a::{ordered_idom,number_ring}) < n",
    1.72        "(m::'a::{ordered_idom,number_ring}) <= n",
    1.73        "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
    1.74  
    1.75  Addsimprocs [fast_int_arith_simproc];
    1.76 -
    1.77 -
    1.78 -(* Some test data
    1.79 -Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    1.80 -by (fast_arith_tac 1);
    1.81 -Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
    1.82 -by (fast_arith_tac 1);
    1.83 -Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d";
    1.84 -by (fast_arith_tac 1);
    1.85 -Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
    1.86 -by (fast_arith_tac 1);
    1.87 -Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
    1.88 -\     ==> a+a <= j+j";
    1.89 -by (fast_arith_tac 1);
    1.90 -Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
    1.91 -\     ==> a+a - - -1 < j+j - 3";
    1.92 -by (fast_arith_tac 1);
    1.93 -Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    1.94 -by (arith_tac 1);
    1.95 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.96 -\     ==> a <= l";
    1.97 -by (fast_arith_tac 1);
    1.98 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.99 -\     ==> a+a+a+a <= l+l+l+l";
   1.100 -by (fast_arith_tac 1);
   1.101 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.102 -\     ==> a+a+a+a+a <= l+l+l+l+i";
   1.103 -by (fast_arith_tac 1);
   1.104 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.105 -\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   1.106 -by (fast_arith_tac 1);
   1.107 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.108 -\     ==> 6*a <= 5*l+i";
   1.109 -by (fast_arith_tac 1);
   1.110 -*)
     2.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Mar 29 11:59:54 2007 +0200
     2.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Mar 29 14:21:45 2007 +0200
     2.3 @@ -54,10 +54,9 @@
     2.4  
     2.5    val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
     2.6    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
     2.7 -  val simplify_meta_eq = 
     2.8 -	Int_Numeral_Simprocs.simplify_meta_eq
     2.9 -	     [add_0, add_0_right,
    2.10 -	      mult_zero_left, mult_zero_right, mult_num1, mult_1_right];
    2.11 +  val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
    2.12 +    [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
    2.13 +      @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
    2.14    end
    2.15  
    2.16  (*Version for integer division*)
    2.17 @@ -76,7 +75,7 @@
    2.18    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.19    val mk_bal   = HOLogic.mk_binop "HOL.divide"
    2.20    val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
    2.21 -  val cancel = mult_divide_cancel_left RS trans
    2.22 +  val cancel = @{thm mult_divide_cancel_left} RS trans
    2.23    val neg_exchanges = false
    2.24  )
    2.25  
    2.26 @@ -86,7 +85,7 @@
    2.27    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.28    val mk_bal   = HOLogic.mk_eq
    2.29    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    2.30 -  val cancel = mult_cancel_left RS trans
    2.31 +  val cancel = @{thm mult_cancel_left} RS trans
    2.32    val neg_exchanges = false
    2.33  )
    2.34  
    2.35 @@ -96,7 +95,7 @@
    2.36    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.37    val mk_bal   = HOLogic.mk_eq
    2.38    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    2.39 -  val cancel = field_mult_cancel_left RS trans
    2.40 +  val cancel = @{thm field_mult_cancel_left} RS trans
    2.41    val neg_exchanges = false
    2.42  )
    2.43  
    2.44 @@ -105,7 +104,7 @@
    2.45    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.46    val mk_bal   = HOLogic.mk_binrel "Orderings.less"
    2.47    val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
    2.48 -  val cancel = mult_less_cancel_left RS trans
    2.49 +  val cancel = @{thm mult_less_cancel_left} RS trans
    2.50    val neg_exchanges = true
    2.51  )
    2.52  
    2.53 @@ -114,7 +113,7 @@
    2.54    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.55    val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
    2.56    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
    2.57 -  val cancel = mult_le_cancel_left RS trans
    2.58 +  val cancel = @{thm mult_le_cancel_left} RS trans
    2.59    val neg_exchanges = true
    2.60  )
    2.61  
    2.62 @@ -236,9 +235,8 @@
    2.63          handle TERM _ => find_first_t (t::past) u terms;
    2.64  
    2.65  (** Final simplification for the CancelFactor simprocs **)
    2.66 -val simplify_one = 
    2.67 -    Int_Numeral_Simprocs.simplify_meta_eq  
    2.68 -       [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
    2.69 +val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
    2.70 +  [@{thm mult_1_left}, mult_1_right, zdiv_1, numeral_1_eq_1];
    2.71  
    2.72  fun cancel_simplify_meta_eq cancel_th ss th =
    2.73      simplify_one ss (([th, cancel_th]) MRS trans);
    2.74 @@ -264,7 +262,7 @@
    2.75    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.76    val mk_bal   = HOLogic.mk_eq
    2.77    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    2.78 -  val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
    2.79 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
    2.80  );
    2.81  
    2.82  (*int_mult_div_cancel_disj is for integer division (div). The version in
    2.83 @@ -291,7 +289,7 @@
    2.84    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.85    val mk_bal   = HOLogic.mk_eq
    2.86    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    2.87 -  val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
    2.88 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm field_mult_cancel_left}
    2.89  );
    2.90  
    2.91  structure FieldDivideCancelFactor = ExtractCommonTermFun
    2.92 @@ -299,7 +297,7 @@
    2.93    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    2.94    val mk_bal   = HOLogic.mk_binop "HOL.divide"
    2.95    val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
    2.96 -  val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
    2.97 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}
    2.98  );
    2.99  
   2.100  (*The number_ring class is necessary because the simprocs refer to the
     3.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Mar 29 11:59:54 2007 +0200
     3.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Mar 29 14:21:45 2007 +0200
     3.3 @@ -351,9 +351,8 @@
     3.4          handle TERM _ => find_first_t (t::past) u terms;
     3.5  
     3.6  (** Final simplification for the CancelFactor simprocs **)
     3.7 -val simplify_one = 
     3.8 -    Int_Numeral_Simprocs.simplify_meta_eq  
     3.9 -       [mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
    3.10 +val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
    3.11 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
    3.12  
    3.13  fun cancel_simplify_meta_eq cancel_th ss th =
    3.14      simplify_one ss (([th, cancel_th]) MRS trans);
    3.15 @@ -538,8 +537,8 @@
    3.16     eq_number_of_0, eq_0_number_of, less_0_number_of,
    3.17     of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False];
    3.18  
    3.19 -val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@
    3.20 -                Nat_Numeral_Simprocs.cancel_numerals;
    3.21 +val simprocs = Nat_Numeral_Simprocs.combine_numerals
    3.22 +  :: Nat_Numeral_Simprocs.cancel_numerals;
    3.23  
    3.24  in
    3.25  
     4.1 --- a/src/HOL/Integ/presburger.ML	Thu Mar 29 11:59:54 2007 +0200
     4.2 +++ b/src/HOL/Integ/presburger.ML	Thu Mar 29 14:21:45 2007 +0200
     4.3 @@ -301,9 +301,9 @@
     4.4                          addsimps add_ac
     4.5                          addsimprocs [cancel_div_mod_proc]
     4.6      val simpset0 = HOL_basic_ss
     4.7 -      addsimps [mod_div_equality', Suc_plus1]
     4.8 +      addsimps [@{thm mod_div_equality'}, @{thm Suc_plus1}]
     4.9        addsimps comp_arith
    4.10 -      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
    4.11 +      addsplits [split_zdiv, split_zmod, split_div', @{thm split_min}, @{thm split_max}]
    4.12      (* Simp rules for changing (n::int) to int n *)
    4.13      val simpset1 = HOL_basic_ss
    4.14        addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
     5.1 --- a/src/HOL/Lattices.thy	Thu Mar 29 11:59:54 2007 +0200
     5.2 +++ b/src/HOL/Lattices.thy	Thu Mar 29 14:21:45 2007 +0200
     5.3 @@ -327,30 +327,4 @@
     5.4  lemmas inf_aci = inf_ACI
     5.5  lemmas sup_aci = sup_ACI
     5.6  
     5.7 -
     5.8 -text {* ML legacy bindings *}
     5.9 -
    5.10 -ML {*
    5.11 -val Least_def = @{thm Least_def}
    5.12 -val Least_equality = @{thm Least_equality}
    5.13 -val min_def = @{thm min_def}
    5.14 -val min_of_mono = @{thm min_of_mono}
    5.15 -val max_def = @{thm max_def}
    5.16 -val max_of_mono = @{thm max_of_mono}
    5.17 -val min_leastL = @{thm min_leastL}
    5.18 -val max_leastL = @{thm max_leastL}
    5.19 -val min_leastR = @{thm min_leastR}
    5.20 -val max_leastR = @{thm max_leastR}
    5.21 -val le_max_iff_disj = @{thm le_max_iff_disj}
    5.22 -val le_maxI1 = @{thm le_maxI1}
    5.23 -val le_maxI2 = @{thm le_maxI2}
    5.24 -val less_max_iff_disj = @{thm less_max_iff_disj}
    5.25 -val max_less_iff_conj = @{thm max_less_iff_conj}
    5.26 -val min_less_iff_conj = @{thm min_less_iff_conj}
    5.27 -val min_le_iff_disj = @{thm min_le_iff_disj}
    5.28 -val min_less_iff_disj = @{thm min_less_iff_disj}
    5.29 -val split_min = @{thm split_min}
    5.30 -val split_max = @{thm split_max}
    5.31 -*}
    5.32 -
    5.33  end
     6.1 --- a/src/HOL/OrderedGroup.thy	Thu Mar 29 11:59:54 2007 +0200
     6.2 +++ b/src/HOL/OrderedGroup.thy	Thu Mar 29 14:21:45 2007 +0200
     6.3 @@ -1088,13 +1088,13 @@
     6.4     @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
     6.5     @{thm minus_add_cancel}];
     6.6    
     6.7 -val eq_reflection = @{thm eq_reflection}
     6.8 +val eq_reflection = @{thm eq_reflection};
     6.9    
    6.10 -val thy_ref = Theory.self_ref @{theory}
    6.11 +val thy_ref = Theory.self_ref @{theory};
    6.12  
    6.13 -val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    6.14 +val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
    6.15  
    6.16 -val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]
    6.17 +val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
    6.18  
    6.19  val dest_eqI = 
    6.20    fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
    6.21 @@ -1106,140 +1106,4 @@
    6.22    Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
    6.23  *}
    6.24  
    6.25 -ML {*
    6.26 -val add_assoc = thm "add_assoc";
    6.27 -val add_commute = thm "add_commute";
    6.28 -val add_left_commute = thm "add_left_commute";
    6.29 -val add_ac = thms "add_ac";
    6.30 -val mult_assoc = thm "mult_assoc";
    6.31 -val mult_commute = thm "mult_commute";
    6.32 -val mult_left_commute = thm "mult_left_commute";
    6.33 -val mult_ac = thms "mult_ac";
    6.34 -val add_0 = thm "add_0";
    6.35 -val mult_1_left = thm "mult_1_left";
    6.36 -val mult_1_right = thm "mult_1_right";
    6.37 -val mult_1 = thm "mult_1";
    6.38 -val add_left_imp_eq = thm "add_left_imp_eq";
    6.39 -val add_right_imp_eq = thm "add_right_imp_eq";
    6.40 -val add_imp_eq = thm "add_imp_eq";
    6.41 -val left_minus = thm "left_minus";
    6.42 -val diff_minus = thm "diff_minus";
    6.43 -val add_0_right = thm "add_0_right";
    6.44 -val add_left_cancel = thm "add_left_cancel";
    6.45 -val add_right_cancel = thm "add_right_cancel";
    6.46 -val right_minus = thm "right_minus";
    6.47 -val right_minus_eq = thm "right_minus_eq";
    6.48 -val minus_minus = thm "minus_minus";
    6.49 -val equals_zero_I = thm "equals_zero_I";
    6.50 -val minus_zero = thm "minus_zero";
    6.51 -val diff_self = thm "diff_self";
    6.52 -val diff_0 = thm "diff_0";
    6.53 -val diff_0_right = thm "diff_0_right";
    6.54 -val diff_minus_eq_add = thm "diff_minus_eq_add";
    6.55 -val neg_equal_iff_equal = thm "neg_equal_iff_equal";
    6.56 -val neg_equal_0_iff_equal = thm "neg_equal_0_iff_equal";
    6.57 -val neg_0_equal_iff_equal = thm "neg_0_equal_iff_equal";
    6.58 -val equation_minus_iff = thm "equation_minus_iff";
    6.59 -val minus_equation_iff = thm "minus_equation_iff";
    6.60 -val minus_add_distrib = thm "minus_add_distrib";
    6.61 -val minus_diff_eq = thm "minus_diff_eq";
    6.62 -val add_left_mono = thm "add_left_mono";
    6.63 -val add_le_imp_le_left = thm "add_le_imp_le_left";
    6.64 -val add_right_mono = thm "add_right_mono";
    6.65 -val add_mono = thm "add_mono";
    6.66 -val add_strict_left_mono = thm "add_strict_left_mono";
    6.67 -val add_strict_right_mono = thm "add_strict_right_mono";
    6.68 -val add_strict_mono = thm "add_strict_mono";
    6.69 -val add_less_le_mono = thm "add_less_le_mono";
    6.70 -val add_le_less_mono = thm "add_le_less_mono";
    6.71 -val add_less_imp_less_left = thm "add_less_imp_less_left";
    6.72 -val add_less_imp_less_right = thm "add_less_imp_less_right";
    6.73 -val add_less_cancel_left = thm "add_less_cancel_left";
    6.74 -val add_less_cancel_right = thm "add_less_cancel_right";
    6.75 -val add_le_cancel_left = thm "add_le_cancel_left";
    6.76 -val add_le_cancel_right = thm "add_le_cancel_right";
    6.77 -val add_le_imp_le_right = thm "add_le_imp_le_right";
    6.78 -val add_increasing = thm "add_increasing";
    6.79 -val le_imp_neg_le = thm "le_imp_neg_le";
    6.80 -val neg_le_iff_le = thm "neg_le_iff_le";
    6.81 -val neg_le_0_iff_le = thm "neg_le_0_iff_le";
    6.82 -val neg_0_le_iff_le = thm "neg_0_le_iff_le";
    6.83 -val neg_less_iff_less = thm "neg_less_iff_less";
    6.84 -val neg_less_0_iff_less = thm "neg_less_0_iff_less";
    6.85 -val neg_0_less_iff_less = thm "neg_0_less_iff_less";
    6.86 -val less_minus_iff = thm "less_minus_iff";
    6.87 -val minus_less_iff = thm "minus_less_iff";
    6.88 -val le_minus_iff = thm "le_minus_iff";
    6.89 -val minus_le_iff = thm "minus_le_iff";
    6.90 -val add_diff_eq = thm "add_diff_eq";
    6.91 -val diff_add_eq = thm "diff_add_eq";
    6.92 -val diff_eq_eq = thm "diff_eq_eq";
    6.93 -val eq_diff_eq = thm "eq_diff_eq";
    6.94 -val diff_diff_eq = thm "diff_diff_eq";
    6.95 -val diff_diff_eq2 = thm "diff_diff_eq2";
    6.96 -val diff_add_cancel = thm "diff_add_cancel";
    6.97 -val add_diff_cancel = thm "add_diff_cancel";
    6.98 -val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
    6.99 -val diff_less_eq = thm "diff_less_eq";
   6.100 -val less_diff_eq = thm "less_diff_eq";
   6.101 -val diff_le_eq = thm "diff_le_eq";
   6.102 -val le_diff_eq = thm "le_diff_eq";
   6.103 -val compare_rls = thms "compare_rls";
   6.104 -val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
   6.105 -val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
   6.106 -val add_inf_distrib_left = thm "add_inf_distrib_left";
   6.107 -val add_sup_distrib_left = thm "add_sup_distrib_left";
   6.108 -val add_sup_distrib_right = thm "add_sup_distrib_right";
   6.109 -val add_inf_distrib_right = thm "add_inf_distrib_right";
   6.110 -val add_sup_inf_distribs = thms "add_sup_inf_distribs";
   6.111 -val sup_eq_neg_inf = thm "sup_eq_neg_inf";
   6.112 -val inf_eq_neg_sup = thm "inf_eq_neg_sup";
   6.113 -val add_eq_inf_sup = thm "add_eq_inf_sup";
   6.114 -val prts = thm "prts";
   6.115 -val zero_le_pprt = thm "zero_le_pprt";
   6.116 -val nprt_le_zero = thm "nprt_le_zero";
   6.117 -val le_eq_neg = thm "le_eq_neg";
   6.118 -val sup_0_imp_0 = thm "sup_0_imp_0";
   6.119 -val inf_0_imp_0 = thm "inf_0_imp_0";
   6.120 -val sup_0_eq_0 = thm "sup_0_eq_0";
   6.121 -val inf_0_eq_0 = thm "inf_0_eq_0";
   6.122 -val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
   6.123 -val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
   6.124 -val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
   6.125 -val abs_lattice = thm "abs_lattice";
   6.126 -val abs_zero = thm "abs_zero";
   6.127 -val abs_eq_0 = thm "abs_eq_0";
   6.128 -val abs_0_eq = thm "abs_0_eq";
   6.129 -val neg_inf_eq_sup = thm "neg_inf_eq_sup";
   6.130 -val neg_sup_eq_inf = thm "neg_sup_eq_inf";
   6.131 -val sup_eq_if = thm "sup_eq_if";
   6.132 -val abs_if_lattice = thm "abs_if_lattice";
   6.133 -val abs_ge_zero = thm "abs_ge_zero";
   6.134 -val abs_le_zero_iff = thm "abs_le_zero_iff";
   6.135 -val zero_less_abs_iff = thm "zero_less_abs_iff";
   6.136 -val abs_not_less_zero = thm "abs_not_less_zero";
   6.137 -val abs_ge_self = thm "abs_ge_self";
   6.138 -val abs_ge_minus_self = thm "abs_ge_minus_self";
   6.139 -val le_imp_join_eq = thm "sup_absorb2";
   6.140 -val ge_imp_join_eq = thm "sup_absorb1";
   6.141 -val le_imp_meet_eq = thm "inf_absorb1";
   6.142 -val ge_imp_meet_eq = thm "inf_absorb2";
   6.143 -val abs_prts = thm "abs_prts";
   6.144 -val abs_minus_cancel = thm "abs_minus_cancel";
   6.145 -val abs_idempotent = thm "abs_idempotent";
   6.146 -val zero_le_iff_zero_nprt = thm "zero_le_iff_zero_nprt";
   6.147 -val le_zero_iff_zero_pprt = thm "le_zero_iff_zero_pprt";
   6.148 -val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
   6.149 -val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
   6.150 -val iff2imp = thm "iff2imp";
   6.151 -val abs_leI = thm "abs_leI";
   6.152 -val le_minus_self_iff = thm "le_minus_self_iff";
   6.153 -val minus_le_self_iff = thm "minus_le_self_iff";
   6.154 -val abs_le_D1 = thm "abs_le_D1";
   6.155 -val abs_le_D2 = thm "abs_le_D2";
   6.156 -val abs_le_iff = thm "abs_le_iff";
   6.157 -val abs_triangle_ineq = thm "abs_triangle_ineq";
   6.158 -val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
   6.159 -*}
   6.160 -
   6.161  end
     7.1 --- a/src/HOL/Orderings.thy	Thu Mar 29 11:59:54 2007 +0200
     7.2 +++ b/src/HOL/Orderings.thy	Thu Mar 29 14:21:45 2007 +0200
     7.3 @@ -901,26 +901,12 @@
     7.4      "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
     7.5    by (simp add: max_def)
     7.6  
     7.7 -subsection {* Basic ML bindings *}
     7.8 +
     7.9 +subsection {* legacy ML bindings *}
    7.10  
    7.11  ML {*
    7.12 -val leD = thm "leD";
    7.13 -val leI = thm "leI";
    7.14 -val linorder_neqE = thm "linorder_neqE";
    7.15 -val linorder_neq_iff = thm "linorder_neq_iff";
    7.16 -val linorder_not_le = thm "linorder_not_le";
    7.17 -val linorder_not_less = thm "linorder_not_less";
    7.18 -val monoD = thm "monoD";
    7.19 -val monoI = thm "monoI";
    7.20 -val order_antisym = thm "order_antisym";
    7.21 -val order_less_irrefl = thm "order_less_irrefl";
    7.22 -val order_refl = thm "order_refl";
    7.23 -val order_trans = thm "order_trans";
    7.24 -val split_max = thm "split_max";
    7.25 -val split_min = thm "split_min";
    7.26 -*}
    7.27 +val monoI = @{thm monoI};
    7.28  
    7.29 -ML {*
    7.30  structure HOL =
    7.31  struct
    7.32    val thy = theory "HOL";
     8.1 --- a/src/HOL/Real/ferrante_rackoff.ML	Thu Mar 29 11:59:54 2007 +0200
     8.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Thu Mar 29 14:21:45 2007 +0200
     8.3 @@ -72,7 +72,7 @@
     8.4  val context_ss = simpset_of (the_context ());
     8.5  
     8.6  fun ferrack_tac q i =  ObjectLogic.atomize_tac i
     8.7 -  THEN REPEAT_DETERM (split_tac [split_min, split_max,abs_split] i)
     8.8 +  THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, abs_split] i)
     8.9    THEN (fn st =>
    8.10    let
    8.11      val g = nth (prems_of st) (i - 1)
    8.12 @@ -80,7 +80,7 @@
    8.13      (* Transform the term*)
    8.14      val (t,np,nh) = prepare_for_linr q g
    8.15      (* Some simpsets for dealing with mod div abs and nat*)
    8.16 -    val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
    8.17 +    val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}]
    8.18      (* simp rules for elimination of abs *)
    8.19      val simpset3 = HOL_basic_ss addsplits [abs_split]
    8.20      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     9.1 --- a/src/HOL/Real/ferrante_rackoff_proof.ML	Thu Mar 29 11:59:54 2007 +0200
     9.2 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Thu Mar 29 14:21:45 2007 +0200
     9.3 @@ -319,7 +319,7 @@
     9.4  val ncmul_congh = thm "ncmul_congh";
     9.5  val ncmul_cong = thm "ncmul_cong";
     9.6  fun decomp_ncmulh thy c t = 
     9.7 -    if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] mult_zero_left) else 
     9.8 +    if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] @{thm mult_zero_left}) else 
     9.9      case t of 
    9.10          Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
    9.11          ([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
    10.1 --- a/src/HOL/Real/rat_arith.ML	Thu Mar 29 11:59:54 2007 +0200
    10.2 +++ b/src/HOL/Real/rat_arith.ML	Thu Mar 29 14:21:45 2007 +0200
    10.3 @@ -12,11 +12,11 @@
    10.4  
    10.5  val simprocs = field_cancel_numeral_factors
    10.6  
    10.7 -val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
    10.8 -             inst "a" "(number_of ?v)" right_distrib,
    10.9 -             divide_1, divide_zero_left,
   10.10 -             times_divide_eq_right, times_divide_eq_left,
   10.11 -             minus_divide_left RS sym, minus_divide_right RS sym,
   10.12 +val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
   10.13 +             inst "a" "(number_of ?v)" @{thm right_distrib},
   10.14 +             @{thm divide_1}, @{thm divide_zero_left},
   10.15 +             @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
   10.16 +             @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
   10.17               of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
   10.18               of_int_mult, of_int_of_nat_eq]
   10.19  
   10.20 @@ -32,10 +32,9 @@
   10.21  
   10.22  in
   10.23  
   10.24 -val fast_rat_arith_simproc =
   10.25 - Simplifier.simproc (the_context ())
   10.26 +val fast_rat_arith_simproc = Simplifier.simproc @{theory}
   10.27    "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
   10.28 -  Fast_Arith.lin_arith_prover
   10.29 +    Fast_Arith.lin_arith_prover
   10.30  
   10.31  val ratT = Type ("Rational.rat", [])
   10.32  
    11.1 --- a/src/HOL/Ring_and_Field.thy	Thu Mar 29 11:59:54 2007 +0200
    11.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Mar 29 14:21:45 2007 +0200
    11.3 @@ -2067,210 +2067,4 @@
    11.4    then show ?thesis by simp
    11.5  qed
    11.6  
    11.7 -ML {*
    11.8 -val left_distrib = thm "left_distrib";
    11.9 -val right_distrib = thm "right_distrib";
   11.10 -val mult_commute = thm "mult_commute";
   11.11 -val distrib = thm "distrib";
   11.12 -val zero_neq_one = thm "zero_neq_one";
   11.13 -val no_zero_divisors = thm "no_zero_divisors";
   11.14 -val left_inverse = thm "left_inverse";
   11.15 -val divide_inverse = thm "divide_inverse";
   11.16 -val mult_zero_left = thm "mult_zero_left";
   11.17 -val mult_zero_right = thm "mult_zero_right";
   11.18 -val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
   11.19 -val inverse_zero = thm "inverse_zero";
   11.20 -val ring_distrib = thms "ring_distrib";
   11.21 -val combine_common_factor = thm "combine_common_factor";
   11.22 -val minus_mult_left = thm "minus_mult_left";
   11.23 -val minus_mult_right = thm "minus_mult_right";
   11.24 -val minus_mult_minus = thm "minus_mult_minus";
   11.25 -val minus_mult_commute = thm "minus_mult_commute";
   11.26 -val right_diff_distrib = thm "right_diff_distrib";
   11.27 -val left_diff_distrib = thm "left_diff_distrib";
   11.28 -val mult_left_mono = thm "mult_left_mono";
   11.29 -val mult_right_mono = thm "mult_right_mono";
   11.30 -val mult_strict_left_mono = thm "mult_strict_left_mono";
   11.31 -val mult_strict_right_mono = thm "mult_strict_right_mono";
   11.32 -val mult_mono = thm "mult_mono";
   11.33 -val mult_strict_mono = thm "mult_strict_mono";
   11.34 -val abs_if = thm "abs_if";
   11.35 -val zero_less_one = thm "zero_less_one";
   11.36 -val eq_add_iff1 = thm "eq_add_iff1";
   11.37 -val eq_add_iff2 = thm "eq_add_iff2";
   11.38 -val less_add_iff1 = thm "less_add_iff1";
   11.39 -val less_add_iff2 = thm "less_add_iff2";
   11.40 -val le_add_iff1 = thm "le_add_iff1";
   11.41 -val le_add_iff2 = thm "le_add_iff2";
   11.42 -val mult_left_le_imp_le = thm "mult_left_le_imp_le";
   11.43 -val mult_right_le_imp_le = thm "mult_right_le_imp_le";
   11.44 -val mult_left_less_imp_less = thm "mult_left_less_imp_less";
   11.45 -val mult_right_less_imp_less = thm "mult_right_less_imp_less";
   11.46 -val mult_strict_left_mono_neg = thm "mult_strict_left_mono_neg";
   11.47 -val mult_left_mono_neg = thm "mult_left_mono_neg";
   11.48 -val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
   11.49 -val mult_right_mono_neg = thm "mult_right_mono_neg";
   11.50 -(*
   11.51 -val mult_pos = thm "mult_pos";
   11.52 -val mult_pos_le = thm "mult_pos_le";
   11.53 -val mult_pos_neg = thm "mult_pos_neg";
   11.54 -val mult_pos_neg_le = thm "mult_pos_neg_le";
   11.55 -val mult_pos_neg2 = thm "mult_pos_neg2";
   11.56 -val mult_pos_neg2_le = thm "mult_pos_neg2_le";
   11.57 -val mult_neg = thm "mult_neg";
   11.58 -val mult_neg_le = thm "mult_neg_le";
   11.59 -*)
   11.60 -val zero_less_mult_pos = thm "zero_less_mult_pos";
   11.61 -val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
   11.62 -val zero_less_mult_iff = thm "zero_less_mult_iff";
   11.63 -val mult_eq_0_iff = thm "mult_eq_0_iff";
   11.64 -val zero_le_mult_iff = thm "zero_le_mult_iff";
   11.65 -val mult_less_0_iff = thm "mult_less_0_iff";
   11.66 -val mult_le_0_iff = thm "mult_le_0_iff";
   11.67 -val split_mult_pos_le = thm "split_mult_pos_le";
   11.68 -val split_mult_neg_le = thm "split_mult_neg_le";
   11.69 -val zero_le_square = thm "zero_le_square";
   11.70 -val zero_le_one = thm "zero_le_one";
   11.71 -val not_one_le_zero = thm "not_one_le_zero";
   11.72 -val not_one_less_zero = thm "not_one_less_zero";
   11.73 -val mult_left_mono_neg = thm "mult_left_mono_neg";
   11.74 -val mult_right_mono_neg = thm "mult_right_mono_neg";
   11.75 -val mult_strict_mono = thm "mult_strict_mono";
   11.76 -val mult_strict_mono' = thm "mult_strict_mono'";
   11.77 -val mult_mono = thm "mult_mono";
   11.78 -val less_1_mult = thm "less_1_mult";
   11.79 -val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";
   11.80 -val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";
   11.81 -val mult_less_cancel_right = thm "mult_less_cancel_right";
   11.82 -val mult_less_cancel_left = thm "mult_less_cancel_left";
   11.83 -val mult_le_cancel_right = thm "mult_le_cancel_right";
   11.84 -val mult_le_cancel_left = thm "mult_le_cancel_left";
   11.85 -val mult_less_imp_less_left = thm "mult_less_imp_less_left";
   11.86 -val mult_less_imp_less_right = thm "mult_less_imp_less_right";
   11.87 -val mult_cancel_right = thm "mult_cancel_right";
   11.88 -val mult_cancel_left = thm "mult_cancel_left";
   11.89 -val ring_eq_simps = thms "ring_eq_simps";
   11.90 -val right_inverse = thm "right_inverse";
   11.91 -val right_inverse_eq = thm "right_inverse_eq";
   11.92 -val nonzero_inverse_eq_divide = thm "nonzero_inverse_eq_divide";
   11.93 -val divide_self = thm "divide_self";
   11.94 -val divide_zero = thm "divide_zero";
   11.95 -val divide_zero_left = thm "divide_zero_left";
   11.96 -val inverse_eq_divide = thm "inverse_eq_divide";
   11.97 -val add_divide_distrib = thm "add_divide_distrib";
   11.98 -val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
   11.99 -val field_mult_cancel_right_lemma = thm "field_mult_cancel_right_lemma";
  11.100 -val field_mult_cancel_right = thm "field_mult_cancel_right";
  11.101 -val field_mult_cancel_left = thm "field_mult_cancel_left";
  11.102 -val nonzero_imp_inverse_nonzero = thm "nonzero_imp_inverse_nonzero";
  11.103 -val inverse_zero_imp_zero = thm "inverse_zero_imp_zero";
  11.104 -val inverse_nonzero_imp_nonzero = thm "inverse_nonzero_imp_nonzero";
  11.105 -val inverse_nonzero_iff_nonzero = thm "inverse_nonzero_iff_nonzero";
  11.106 -val nonzero_inverse_minus_eq = thm "nonzero_inverse_minus_eq";
  11.107 -val inverse_minus_eq = thm "inverse_minus_eq";
  11.108 -val nonzero_inverse_eq_imp_eq = thm "nonzero_inverse_eq_imp_eq";
  11.109 -val inverse_eq_imp_eq = thm "inverse_eq_imp_eq";
  11.110 -val inverse_eq_iff_eq = thm "inverse_eq_iff_eq";
  11.111 -val nonzero_inverse_inverse_eq = thm "nonzero_inverse_inverse_eq";
  11.112 -val inverse_inverse_eq = thm "inverse_inverse_eq";
  11.113 -val inverse_1 = thm "inverse_1";
  11.114 -val nonzero_inverse_mult_distrib = thm "nonzero_inverse_mult_distrib";
  11.115 -val inverse_mult_distrib = thm "inverse_mult_distrib";
  11.116 -val inverse_add = thm "inverse_add";
  11.117 -val inverse_divide = thm "inverse_divide";
  11.118 -val nonzero_mult_divide_cancel_left = thm "nonzero_mult_divide_cancel_left";
  11.119 -val mult_divide_cancel_left = thm "mult_divide_cancel_left";
  11.120 -val nonzero_mult_divide_cancel_right = thm "nonzero_mult_divide_cancel_right";
  11.121 -val mult_divide_cancel_right = thm "mult_divide_cancel_right";
  11.122 -val mult_divide_cancel_eq_if = thm "mult_divide_cancel_eq_if";
  11.123 -val divide_1 = thm "divide_1";
  11.124 -val times_divide_eq_right = thm "times_divide_eq_right";
  11.125 -val times_divide_eq_left = thm "times_divide_eq_left";
  11.126 -val divide_divide_eq_right = thm "divide_divide_eq_right";
  11.127 -val divide_divide_eq_left = thm "divide_divide_eq_left";
  11.128 -val nonzero_minus_divide_left = thm "nonzero_minus_divide_left";
  11.129 -val nonzero_minus_divide_right = thm "nonzero_minus_divide_right";
  11.130 -val nonzero_minus_divide_divide = thm "nonzero_minus_divide_divide";
  11.131 -val minus_divide_left = thm "minus_divide_left";
  11.132 -val minus_divide_right = thm "minus_divide_right";
  11.133 -val minus_divide_divide = thm "minus_divide_divide";
  11.134 -val diff_divide_distrib = thm "diff_divide_distrib";
  11.135 -val positive_imp_inverse_positive = thm "positive_imp_inverse_positive";
  11.136 -val negative_imp_inverse_negative = thm "negative_imp_inverse_negative";
  11.137 -val inverse_le_imp_le = thm "inverse_le_imp_le";
  11.138 -val inverse_positive_imp_positive = thm "inverse_positive_imp_positive";
  11.139 -val inverse_positive_iff_positive = thm "inverse_positive_iff_positive";
  11.140 -val inverse_negative_imp_negative = thm "inverse_negative_imp_negative";
  11.141 -val inverse_negative_iff_negative = thm "inverse_negative_iff_negative";
  11.142 -val inverse_nonnegative_iff_nonnegative = thm "inverse_nonnegative_iff_nonnegative";
  11.143 -val inverse_nonpositive_iff_nonpositive = thm "inverse_nonpositive_iff_nonpositive";
  11.144 -val less_imp_inverse_less = thm "less_imp_inverse_less";
  11.145 -val inverse_less_imp_less = thm "inverse_less_imp_less";
  11.146 -val inverse_less_iff_less = thm "inverse_less_iff_less";
  11.147 -val le_imp_inverse_le = thm "le_imp_inverse_le";
  11.148 -val inverse_le_iff_le = thm "inverse_le_iff_le";
  11.149 -val inverse_le_imp_le_neg = thm "inverse_le_imp_le_neg";
  11.150 -val less_imp_inverse_less_neg = thm "less_imp_inverse_less_neg";
  11.151 -val inverse_less_imp_less_neg = thm "inverse_less_imp_less_neg";
  11.152 -val inverse_less_iff_less_neg = thm "inverse_less_iff_less_neg";
  11.153 -val le_imp_inverse_le_neg = thm "le_imp_inverse_le_neg";
  11.154 -val inverse_le_iff_le_neg = thm "inverse_le_iff_le_neg";
  11.155 -val one_less_inverse_iff = thm "one_less_inverse_iff";
  11.156 -val inverse_eq_1_iff = thm "inverse_eq_1_iff";
  11.157 -val one_le_inverse_iff = thm "one_le_inverse_iff";
  11.158 -val inverse_less_1_iff = thm "inverse_less_1_iff";
  11.159 -val inverse_le_1_iff = thm "inverse_le_1_iff";
  11.160 -val zero_less_divide_iff = thm "zero_less_divide_iff";
  11.161 -val divide_less_0_iff = thm "divide_less_0_iff";
  11.162 -val zero_le_divide_iff = thm "zero_le_divide_iff";
  11.163 -val divide_le_0_iff = thm "divide_le_0_iff";
  11.164 -val divide_eq_0_iff = thm "divide_eq_0_iff";
  11.165 -val pos_le_divide_eq = thm "pos_le_divide_eq";
  11.166 -val neg_le_divide_eq = thm "neg_le_divide_eq";
  11.167 -val le_divide_eq = thm "le_divide_eq";
  11.168 -val pos_divide_le_eq = thm "pos_divide_le_eq";
  11.169 -val neg_divide_le_eq = thm "neg_divide_le_eq";
  11.170 -val divide_le_eq = thm "divide_le_eq";
  11.171 -val pos_less_divide_eq = thm "pos_less_divide_eq";
  11.172 -val neg_less_divide_eq = thm "neg_less_divide_eq";
  11.173 -val less_divide_eq = thm "less_divide_eq";
  11.174 -val pos_divide_less_eq = thm "pos_divide_less_eq";
  11.175 -val neg_divide_less_eq = thm "neg_divide_less_eq";
  11.176 -val divide_less_eq = thm "divide_less_eq";
  11.177 -val nonzero_eq_divide_eq = thm "nonzero_eq_divide_eq";
  11.178 -val eq_divide_eq = thm "eq_divide_eq";
  11.179 -val nonzero_divide_eq_eq = thm "nonzero_divide_eq_eq";
  11.180 -val divide_eq_eq = thm "divide_eq_eq";
  11.181 -val divide_cancel_right = thm "divide_cancel_right";
  11.182 -val divide_cancel_left = thm "divide_cancel_left";
  11.183 -val divide_eq_1_iff = thm "divide_eq_1_iff";
  11.184 -val one_eq_divide_iff = thm "one_eq_divide_iff";
  11.185 -val zero_eq_1_divide_iff = thm "zero_eq_1_divide_iff";
  11.186 -val one_divide_eq_0_iff = thm "one_divide_eq_0_iff";
  11.187 -val divide_strict_right_mono = thm "divide_strict_right_mono";
  11.188 -val divide_right_mono = thm "divide_right_mono";
  11.189 -val divide_strict_left_mono = thm "divide_strict_left_mono";
  11.190 -val divide_left_mono = thm "divide_left_mono";
  11.191 -val divide_strict_left_mono_neg = thm "divide_strict_left_mono_neg";
  11.192 -val divide_strict_right_mono_neg = thm "divide_strict_right_mono_neg";
  11.193 -val less_add_one = thm "less_add_one";
  11.194 -val zero_less_two = thm "zero_less_two";
  11.195 -val less_half_sum = thm "less_half_sum";
  11.196 -val gt_half_sum = thm "gt_half_sum";
  11.197 -val dense = thm "dense";
  11.198 -val abs_one = thm "abs_one";
  11.199 -val abs_le_mult = thm "abs_le_mult";
  11.200 -val abs_eq_mult = thm "abs_eq_mult";
  11.201 -val abs_mult = thm "abs_mult";
  11.202 -val abs_mult_self = thm "abs_mult_self";
  11.203 -val nonzero_abs_inverse = thm "nonzero_abs_inverse";
  11.204 -val abs_inverse = thm "abs_inverse";
  11.205 -val nonzero_abs_divide = thm "nonzero_abs_divide";
  11.206 -val abs_divide = thm "abs_divide";
  11.207 -val abs_mult_less = thm "abs_mult_less";
  11.208 -val eq_minus_self_iff = thm "eq_minus_self_iff";
  11.209 -val less_minus_self_iff = thm "less_minus_self_iff";
  11.210 -val abs_less_iff = thm "abs_less_iff";
  11.211 -*}
  11.212 -
  11.213  end
    12.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Mar 29 11:59:54 2007 +0200
    12.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Mar 29 14:21:45 2007 +0200
    12.3 @@ -301,9 +301,9 @@
    12.4                          addsimps add_ac
    12.5                          addsimprocs [cancel_div_mod_proc]
    12.6      val simpset0 = HOL_basic_ss
    12.7 -      addsimps [mod_div_equality', Suc_plus1]
    12.8 +      addsimps [@{thm mod_div_equality'}, @{thm Suc_plus1}]
    12.9        addsimps comp_arith
   12.10 -      addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
   12.11 +      addsplits [split_zdiv, split_zmod, split_div', @{thm split_min}, @{thm split_max}]
   12.12      (* Simp rules for changing (n::int) to int n *)
   12.13      val simpset1 = HOL_basic_ss
   12.14        addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
    13.1 --- a/src/HOL/W0/W0.thy	Thu Mar 29 11:59:54 2007 +0200
    13.2 +++ b/src/HOL/W0/W0.thy	Thu Mar 29 14:21:45 2007 +0200
    13.3 @@ -196,7 +196,7 @@
    13.4    apply (unfold new_tv_def)
    13.5    apply (tactic "safe_tac HOL_cs")
    13.6    -- {* @{text \<Longrightarrow>} *}
    13.7 -    apply (tactic {* fast_tac (HOL_cs addDs [leD] addss (simpset()
    13.8 +    apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (simpset()
    13.9        addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
   13.10     apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
   13.11      apply (tactic "safe_tac HOL_cs")
    14.1 --- a/src/HOL/arith_data.ML	Thu Mar 29 11:59:54 2007 +0200
    14.2 +++ b/src/HOL/arith_data.ML	Thu Mar 29 14:21:45 2007 +0200
    14.3 @@ -89,7 +89,7 @@
    14.4    val dest_sum = dest_sum;
    14.5    val prove_conv = prove_conv;
    14.6    val norm_tac1 = simp_all_tac add_rules;
    14.7 -  val norm_tac2 = simp_all_tac add_ac;
    14.8 +  val norm_tac2 = simp_all_tac @{thms add_ac};
    14.9    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
   14.10  end;
   14.11  
   14.12 @@ -172,8 +172,8 @@
   14.13  val conjI = conjI;
   14.14  val notI = notI;
   14.15  val sym = sym;
   14.16 -val not_lessD = linorder_not_less RS iffD1;
   14.17 -val not_leD = linorder_not_le RS iffD1;
   14.18 +val not_lessD = @{thm linorder_not_less} RS iffD1;
   14.19 +val not_leD = @{thm linorder_not_le} RS iffD1;
   14.20  val le0 = thm "le0";
   14.21  
   14.22  fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   14.23 @@ -937,7 +937,7 @@
   14.24  
   14.25  val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
   14.26   (fn prems => [cut_facts_tac prems 1,
   14.27 -               blast_tac (claset() addIs [add_mono]) 1]))
   14.28 +               blast_tac (claset() addIs [@{thm add_mono}]) 1]))
   14.29  ["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
   14.30   "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
   14.31   "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
   14.32 @@ -945,7 +945,8 @@
   14.33  ];
   14.34  
   14.35  val mono_ss = simpset() addsimps
   14.36 -                [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
   14.37 +  [@{thm add_mono}, @{thm add_strict_mono},
   14.38 +     @{thm add_less_le_mono}, @{thm add_le_less_mono}];
   14.39  
   14.40  val add_mono_thms_ordered_field =
   14.41    map (fn s => prove_goal (the_context ()) s
   14.42 @@ -966,7 +967,7 @@
   14.43      mult_mono_thms = mult_mono_thms,
   14.44      inj_thms = inj_thms,
   14.45      lessD = lessD @ [thm "Suc_leI"],
   14.46 -    neqE = [thm "linorder_neqE_nat",
   14.47 +    neqE = [@{thm linorder_neqE_nat},
   14.48        get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
   14.49      simpset = HOL_basic_ss addsimps add_rules
   14.50                     addsimprocs [ab_group_add_cancel.sum_conv,
   14.51 @@ -1041,7 +1042,7 @@
   14.52  
   14.53  local
   14.54  val antisym = mk_meta_eq order_antisym
   14.55 -val not_lessD = linorder_not_less RS iffD1
   14.56 +val not_lessD = @{thm linorder_not_less} RS iffD1
   14.57  fun prp t thm = (#prop(rep_thm thm) = t)
   14.58  in
   14.59  fun antisym_eq prems thm =
    15.1 --- a/src/HOL/ex/MT.ML	Thu Mar 29 11:59:54 2007 +0200
    15.2 +++ b/src/HOL/ex/MT.ML	Thu Mar 29 14:21:45 2007 +0200
    15.3 @@ -81,11 +81,11 @@
    15.4  
    15.5  val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
    15.6  by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
    15.7 -by (rtac (monoh RS monoD) 1);
    15.8 +by (rtac (monoh RS @{thm monoD}) 1);
    15.9  by (rtac (UnE RS subsetI) 1);
   15.10  by (assume_tac 1);
   15.11  by (blast_tac (claset() addSIs [cih]) 1);
   15.12 -by (rtac (monoh RS monoD RS subsetD) 1);
   15.13 +by (rtac (monoh RS @{thm monoD} RS subsetD) 1);
   15.14  by (rtac (thm "Un_upper2") 1);
   15.15  by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
   15.16  qed "gfp_coind2";