src/HOL/int_arith1.ML
changeset 23881 851c74f1bb69
parent 23400 a64b39e5809b
child 24075 366d4d234814
     1.1 --- a/src/HOL/int_arith1.ML	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/src/HOL/int_arith1.ML	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -110,8 +110,8 @@
     1.4        mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
     1.5  
     1.6    (*reorientation simprules using ==, for the following simproc*)
     1.7 -  val meta_zero_reorient = zero_reorient RS eq_reflection
     1.8 -  val meta_one_reorient = one_reorient RS eq_reflection
     1.9 +  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
    1.10 +  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    1.11    val meta_number_of_reorient = number_of_reorient RS eq_reflection
    1.12  
    1.13    (*reorientation simplification procedure: reorients (polymorphic) 
    1.14 @@ -350,9 +350,9 @@
    1.15    val trans_tac         = fn _ => trans_tac
    1.16  
    1.17    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.18 -    diff_simps @ minus_simps @ add_ac
    1.19 +    diff_simps @ minus_simps @ @{thms add_ac}
    1.20    val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.21 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
    1.22 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.23    fun norm_tac ss =
    1.24      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.25      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.26 @@ -376,8 +376,8 @@
    1.27  structure LessCancelNumerals = CancelNumeralsFun
    1.28   (open CancelNumeralsCommon
    1.29    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.30 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
    1.31 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
    1.32 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
    1.33 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
    1.34    val bal_add1 = less_add_iff1 RS trans
    1.35    val bal_add2 = less_add_iff2 RS trans
    1.36  );
    1.37 @@ -385,8 +385,8 @@
    1.38  structure LeCancelNumerals = CancelNumeralsFun
    1.39   (open CancelNumeralsCommon
    1.40    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.41 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
    1.42 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
    1.43 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
    1.44 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
    1.45    val bal_add1 = le_add_iff1 RS trans
    1.46    val bal_add2 = le_add_iff2 RS trans
    1.47  );
    1.48 @@ -433,9 +433,9 @@
    1.49    val trans_tac         = fn _ => trans_tac
    1.50  
    1.51    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.52 -    diff_simps @ minus_simps @ add_ac
    1.53 +    diff_simps @ minus_simps @ @{thms add_ac}
    1.54    val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.55 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
    1.56 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.57    fun norm_tac ss =
    1.58      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.59      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.60 @@ -463,9 +463,9 @@
    1.61    val trans_tac         = fn _ => trans_tac
    1.62  
    1.63    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    1.64 -    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ add_ac
    1.65 +    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
    1.66    val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
    1.67 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
    1.68 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.69    fun norm_tac ss =
    1.70      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.71      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.72 @@ -541,7 +541,7 @@
    1.73  
    1.74  structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
    1.75  struct
    1.76 -  val assoc_ss = HOL_ss addsimps mult_ac
    1.77 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
    1.78    val eq_reflection = eq_reflection
    1.79  end;
    1.80