tuned prove_conv (error reporting done within meta_simplifier.ML);
authorwenzelm
Thu Aug 08 23:50:23 2002 +0200 (2002-08-08)
changeset 13485acf39e924091
parent 13484 d8f5d3391766
child 13486 54464ea94d6f
tuned prove_conv (error reporting done within meta_simplifier.ML);
src/HOL/Hyperreal/HyperArith0.ML
src/HOL/Hyperreal/HyperBin.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_bin.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Real/RealArith0.ML
     1.1 --- a/src/HOL/Hyperreal/HyperArith0.ML	Thu Aug 08 23:49:44 2002 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperArith0.ML	Thu Aug 08 23:50:23 2002 +0200
     1.3 @@ -223,8 +223,7 @@
     1.4  
     1.5  structure DivCancelNumeralFactor = CancelNumeralFactorFun
     1.6   (open CancelNumeralFactorCommon
     1.7 -  val prove_conv = Real_Numeral_Simprocs.prove_conv
     1.8 -                     "hyprealdiv_cancel_numeral_factor"
     1.9 +  val prove_conv = Bin_Simprocs.prove_conv
    1.10    val mk_bal   = HOLogic.mk_binop "HOL.divide"
    1.11    val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
    1.12    val cancel = hypreal_mult_div_cancel1 RS trans
    1.13 @@ -233,8 +232,7 @@
    1.14  
    1.15  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    1.16   (open CancelNumeralFactorCommon
    1.17 -  val prove_conv = Real_Numeral_Simprocs.prove_conv
    1.18 -                     "hyprealeq_cancel_numeral_factor"
    1.19 +  val prove_conv = Bin_Simprocs.prove_conv
    1.20    val mk_bal   = HOLogic.mk_eq
    1.21    val dest_bal = HOLogic.dest_bin "op =" hyprealT
    1.22    val cancel = hypreal_mult_eq_cancel1 RS trans
    1.23 @@ -243,8 +241,7 @@
    1.24  
    1.25  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    1.26   (open CancelNumeralFactorCommon
    1.27 -  val prove_conv = Real_Numeral_Simprocs.prove_conv
    1.28 -                     "hyprealless_cancel_numeral_factor"
    1.29 +  val prove_conv = Bin_Simprocs.prove_conv
    1.30    val mk_bal   = HOLogic.mk_binrel "op <"
    1.31    val dest_bal = HOLogic.dest_bin "op <" hyprealT
    1.32    val cancel = hypreal_mult_less_cancel1 RS trans
    1.33 @@ -253,8 +250,7 @@
    1.34  
    1.35  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    1.36   (open CancelNumeralFactorCommon
    1.37 -  val prove_conv = Real_Numeral_Simprocs.prove_conv
    1.38 -                     "hyprealle_cancel_numeral_factor"
    1.39 +  val prove_conv = Bin_Simprocs.prove_conv
    1.40    val mk_bal   = HOLogic.mk_binrel "op <="
    1.41    val dest_bal = HOLogic.dest_bin "op <=" hyprealT
    1.42    val cancel = hypreal_mult_le_cancel1 RS trans
    1.43 @@ -344,8 +340,7 @@
    1.44  
    1.45  structure EqCancelFactor = ExtractCommonTermFun
    1.46   (open CancelFactorCommon
    1.47 -  val prove_conv = Real_Numeral_Simprocs.prove_conv
    1.48 -                     "hypreal_eq_cancel_factor"
    1.49 +  val prove_conv = Bin_Simprocs.prove_conv
    1.50    val mk_bal   = HOLogic.mk_eq
    1.51    val dest_bal = HOLogic.dest_bin "op =" hyprealT
    1.52    val simplify_meta_eq  = cancel_simplify_meta_eq hypreal_mult_eq_cancel1
    1.53 @@ -354,8 +349,7 @@
    1.54  
    1.55  structure DivideCancelFactor = ExtractCommonTermFun
    1.56   (open CancelFactorCommon
    1.57 -  val prove_conv = Real_Numeral_Simprocs.prove_conv
    1.58 -                     "hypreal_divide_cancel_factor"
    1.59 +  val prove_conv = Bin_Simprocs.prove_conv
    1.60    val mk_bal   = HOLogic.mk_binop "HOL.divide"
    1.61    val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
    1.62    val simplify_meta_eq  = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj
     2.1 --- a/src/HOL/Hyperreal/HyperBin.ML	Thu Aug 08 23:49:44 2002 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperBin.ML	Thu Aug 08 23:50:23 2002 +0200
     2.3 @@ -383,7 +383,7 @@
     2.4  
     2.5  structure EqCancelNumerals = CancelNumeralsFun
     2.6   (open CancelNumeralsCommon
     2.7 -  val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealeq_cancel_numerals"
     2.8 +  val prove_conv = Bin_Simprocs.prove_conv
     2.9    val mk_bal   = HOLogic.mk_eq
    2.10    val dest_bal = HOLogic.dest_bin "op =" hyprealT
    2.11    val bal_add1 = hypreal_eq_add_iff1 RS trans
    2.12 @@ -392,7 +392,7 @@
    2.13  
    2.14  structure LessCancelNumerals = CancelNumeralsFun
    2.15   (open CancelNumeralsCommon
    2.16 -  val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealless_cancel_numerals"
    2.17 +  val prove_conv = Bin_Simprocs.prove_conv
    2.18    val mk_bal   = HOLogic.mk_binrel "op <"
    2.19    val dest_bal = HOLogic.dest_bin "op <" hyprealT
    2.20    val bal_add1 = hypreal_less_add_iff1 RS trans
    2.21 @@ -401,7 +401,7 @@
    2.22  
    2.23  structure LeCancelNumerals = CancelNumeralsFun
    2.24   (open CancelNumeralsCommon
    2.25 -  val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealle_cancel_numerals"
    2.26 +  val prove_conv = Bin_Simprocs.prove_conv
    2.27    val mk_bal   = HOLogic.mk_binrel "op <="
    2.28    val dest_bal = HOLogic.dest_bin "op <=" hyprealT
    2.29    val bal_add1 = hypreal_le_add_iff1 RS trans
    2.30 @@ -435,8 +435,7 @@
    2.31    val mk_coeff          = mk_coeff
    2.32    val dest_coeff        = dest_coeff 1
    2.33    val left_distrib      = left_hypreal_add_mult_distrib RS trans
    2.34 -  val prove_conv        = Real_Numeral_Simprocs.prove_conv_nohyps
    2.35 -                                                "hypreal_combine_numerals"
    2.36 +  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    2.37    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    2.38    val norm_tac =
    2.39       ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    2.40 @@ -483,8 +482,7 @@
    2.41    val is_numeral      = Bin_Simprocs.is_numeral
    2.42    val numeral_0_eq_0  = hypreal_numeral_0_eq_0
    2.43    val numeral_1_eq_1  = hypreal_numeral_1_eq_1
    2.44 -  val prove_conv      = Real_Numeral_Simprocs.prove_conv_nohyps
    2.45 -                          "hypreal_abstract_numerals"
    2.46 +  val prove_conv      = Bin_Simprocs.prove_conv_nohyps_novars
    2.47    fun norm_tac simps  = ALLGOALS (simp_tac (HOL_ss addsimps simps))
    2.48    val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
    2.49    end
     3.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Aug 08 23:49:44 2002 +0200
     3.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Aug 08 23:50:23 2002 +0200
     3.3 @@ -225,7 +225,7 @@
     3.4  
     3.5  structure EqCancelNumerals = CancelNumeralsFun
     3.6   (open CancelNumeralsCommon
     3.7 -  val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numerals"
     3.8 +  val prove_conv = Bin_Simprocs.prove_conv
     3.9    val mk_bal   = HOLogic.mk_eq
    3.10    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    3.11    val bal_add1 = eq_add_iff1 RS trans
    3.12 @@ -234,7 +234,7 @@
    3.13  
    3.14  structure LessCancelNumerals = CancelNumeralsFun
    3.15   (open CancelNumeralsCommon
    3.16 -  val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numerals"
    3.17 +  val prove_conv = Bin_Simprocs.prove_conv
    3.18    val mk_bal   = HOLogic.mk_binrel "op <"
    3.19    val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    3.20    val bal_add1 = less_add_iff1 RS trans
    3.21 @@ -243,7 +243,7 @@
    3.22  
    3.23  structure LeCancelNumerals = CancelNumeralsFun
    3.24   (open CancelNumeralsCommon
    3.25 -  val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numerals"
    3.26 +  val prove_conv = Bin_Simprocs.prove_conv
    3.27    val mk_bal   = HOLogic.mk_binrel "op <="
    3.28    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    3.29    val bal_add1 = le_add_iff1 RS trans
    3.30 @@ -277,7 +277,7 @@
    3.31    val mk_coeff          = mk_coeff
    3.32    val dest_coeff        = dest_coeff 1
    3.33    val left_distrib      = left_zadd_zmult_distrib RS trans
    3.34 -  val prove_conv        = Bin_Simprocs.prove_conv_nohyps "int_combine_numerals"
    3.35 +  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    3.36    val trans_tac          = trans_tac
    3.37    val norm_tac =
    3.38       ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
     4.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Aug 08 23:49:44 2002 +0200
     4.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Aug 08 23:50:23 2002 +0200
     4.3 @@ -54,7 +54,7 @@
     4.4  
     4.5  structure DivCancelNumeralFactor = CancelNumeralFactorFun
     4.6   (open CancelNumeralFactorCommon
     4.7 -  val prove_conv = Bin_Simprocs.prove_conv "intdiv_cancel_numeral_factor"
     4.8 +  val prove_conv = Bin_Simprocs.prove_conv
     4.9    val mk_bal   = HOLogic.mk_binop "Divides.op div"
    4.10    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    4.11    val cancel = int_mult_div_cancel1 RS trans
    4.12 @@ -63,7 +63,7 @@
    4.13  
    4.14  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    4.15   (open CancelNumeralFactorCommon
    4.16 -  val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numeral_factor"
    4.17 +  val prove_conv = Bin_Simprocs.prove_conv
    4.18    val mk_bal   = HOLogic.mk_eq
    4.19    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    4.20    val cancel = int_mult_eq_cancel1 RS trans
    4.21 @@ -72,7 +72,7 @@
    4.22  
    4.23  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    4.24   (open CancelNumeralFactorCommon
    4.25 -  val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numeral_factor"
    4.26 +  val prove_conv = Bin_Simprocs.prove_conv
    4.27    val mk_bal   = HOLogic.mk_binrel "op <"
    4.28    val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    4.29    val cancel = int_mult_less_cancel1 RS trans
    4.30 @@ -81,7 +81,7 @@
    4.31  
    4.32  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    4.33   (open CancelNumeralFactorCommon
    4.34 -  val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numeral_factor"
    4.35 +  val prove_conv = Bin_Simprocs.prove_conv
    4.36    val mk_bal   = HOLogic.mk_binrel "op <="
    4.37    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    4.38    val cancel = int_mult_le_cancel1 RS trans
    4.39 @@ -177,7 +177,7 @@
    4.40  
    4.41  structure EqCancelFactor = ExtractCommonTermFun
    4.42   (open CancelFactorCommon
    4.43 -  val prove_conv = Bin_Simprocs.prove_conv "int_eq_cancel_factor"
    4.44 +  val prove_conv = Bin_Simprocs.prove_conv
    4.45    val mk_bal   = HOLogic.mk_eq
    4.46    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    4.47    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
    4.48 @@ -185,7 +185,7 @@
    4.49  
    4.50  structure DivideCancelFactor = ExtractCommonTermFun
    4.51   (open CancelFactorCommon
    4.52 -  val prove_conv = Bin_Simprocs.prove_conv "int_divide_cancel_factor"
    4.53 +  val prove_conv = Bin_Simprocs.prove_conv
    4.54    val mk_bal   = HOLogic.mk_binop "Divides.op div"
    4.55    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    4.56    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
     5.1 --- a/src/HOL/Integ/nat_bin.ML	Thu Aug 08 23:49:44 2002 +0200
     5.2 +++ b/src/HOL/Integ/nat_bin.ML	Thu Aug 08 23:50:23 2002 +0200
     5.3 @@ -229,7 +229,7 @@
     5.4    val is_numeral	= Bin_Simprocs.is_numeral
     5.5    val numeral_0_eq_0    = numeral_0_eq_0
     5.6    val numeral_1_eq_1    = numeral_1_eq_Suc_0
     5.7 -  val prove_conv   = Bin_Simprocs.prove_conv_nohyps "nat_abstract_numerals"
     5.8 +  val prove_conv        = Bin_Simprocs.prove_conv_nohyps_novars
     5.9    fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
    5.10    val simplify_meta_eq  = Bin_Simprocs.simplify_meta_eq 
    5.11    end
     6.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Aug 08 23:49:44 2002 +0200
     6.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Aug 08 23:50:23 2002 +0200
     6.3 @@ -268,7 +268,7 @@
     6.4  
     6.5  structure EqCancelNumerals = CancelNumeralsFun
     6.6   (open CancelNumeralsCommon
     6.7 -  val prove_conv = Bin_Simprocs.prove_conv "nateq_cancel_numerals"
     6.8 +  val prove_conv = Bin_Simprocs.prove_conv
     6.9    val mk_bal   = HOLogic.mk_eq
    6.10    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
    6.11    val bal_add1 = nat_eq_add_iff1 RS trans
    6.12 @@ -277,7 +277,7 @@
    6.13  
    6.14  structure LessCancelNumerals = CancelNumeralsFun
    6.15   (open CancelNumeralsCommon
    6.16 -  val prove_conv = Bin_Simprocs.prove_conv "natless_cancel_numerals"
    6.17 +  val prove_conv = Bin_Simprocs.prove_conv
    6.18    val mk_bal   = HOLogic.mk_binrel "op <"
    6.19    val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
    6.20    val bal_add1 = nat_less_add_iff1 RS trans
    6.21 @@ -286,7 +286,7 @@
    6.22  
    6.23  structure LeCancelNumerals = CancelNumeralsFun
    6.24   (open CancelNumeralsCommon
    6.25 -  val prove_conv = Bin_Simprocs.prove_conv "natle_cancel_numerals"
    6.26 +  val prove_conv = Bin_Simprocs.prove_conv
    6.27    val mk_bal   = HOLogic.mk_binrel "op <="
    6.28    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
    6.29    val bal_add1 = nat_le_add_iff1 RS trans
    6.30 @@ -295,7 +295,7 @@
    6.31  
    6.32  structure DiffCancelNumerals = CancelNumeralsFun
    6.33   (open CancelNumeralsCommon
    6.34 -  val prove_conv = Bin_Simprocs.prove_conv "natdiff_cancel_numerals"
    6.35 +  val prove_conv = Bin_Simprocs.prove_conv
    6.36    val mk_bal   = HOLogic.mk_binop "op -"
    6.37    val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
    6.38    val bal_add1 = nat_diff_add_eq1 RS trans
    6.39 @@ -337,7 +337,7 @@
    6.40    val mk_coeff          = mk_coeff
    6.41    val dest_coeff        = dest_coeff
    6.42    val left_distrib      = left_add_mult_distrib RS trans
    6.43 -  val prove_conv        = Bin_Simprocs.prove_conv_nohyps "nat_combine_numerals"
    6.44 +  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    6.45    val trans_tac          = trans_tac
    6.46    val norm_tac = ALLGOALS
    6.47                     (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
    6.48 @@ -371,7 +371,7 @@
    6.49  
    6.50  structure DivCancelNumeralFactor = CancelNumeralFactorFun
    6.51   (open CancelNumeralFactorCommon
    6.52 -  val prove_conv = Bin_Simprocs.prove_conv "natdiv_cancel_numeral_factor"
    6.53 +  val prove_conv = Bin_Simprocs.prove_conv
    6.54    val mk_bal   = HOLogic.mk_binop "Divides.op div"
    6.55    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
    6.56    val cancel = nat_mult_div_cancel1 RS trans
    6.57 @@ -380,7 +380,7 @@
    6.58  
    6.59  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    6.60   (open CancelNumeralFactorCommon
    6.61 -  val prove_conv = Bin_Simprocs.prove_conv "nateq_cancel_numeral_factor"
    6.62 +  val prove_conv = Bin_Simprocs.prove_conv
    6.63    val mk_bal   = HOLogic.mk_eq
    6.64    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
    6.65    val cancel = nat_mult_eq_cancel1 RS trans
    6.66 @@ -389,7 +389,7 @@
    6.67  
    6.68  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    6.69   (open CancelNumeralFactorCommon
    6.70 -  val prove_conv = Bin_Simprocs.prove_conv "natless_cancel_numeral_factor"
    6.71 +  val prove_conv = Bin_Simprocs.prove_conv
    6.72    val mk_bal   = HOLogic.mk_binrel "op <"
    6.73    val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
    6.74    val cancel = nat_mult_less_cancel1 RS trans
    6.75 @@ -398,7 +398,7 @@
    6.76  
    6.77  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    6.78   (open CancelNumeralFactorCommon
    6.79 -  val prove_conv = Bin_Simprocs.prove_conv "natle_cancel_numeral_factor"
    6.80 +  val prove_conv = Bin_Simprocs.prove_conv
    6.81    val mk_bal   = HOLogic.mk_binrel "op <="
    6.82    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
    6.83    val cancel = nat_mult_le_cancel1 RS trans
    6.84 @@ -453,7 +453,7 @@
    6.85  
    6.86  structure EqCancelFactor = ExtractCommonTermFun
    6.87   (open CancelFactorCommon
    6.88 -  val prove_conv = Bin_Simprocs.prove_conv "nat_eq_cancel_factor"
    6.89 +  val prove_conv = Bin_Simprocs.prove_conv
    6.90    val mk_bal   = HOLogic.mk_eq
    6.91    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
    6.92    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
    6.93 @@ -461,7 +461,7 @@
    6.94  
    6.95  structure LessCancelFactor = ExtractCommonTermFun
    6.96   (open CancelFactorCommon
    6.97 -  val prove_conv = Bin_Simprocs.prove_conv "nat_less_cancel_factor"
    6.98 +  val prove_conv = Bin_Simprocs.prove_conv
    6.99    val mk_bal   = HOLogic.mk_binrel "op <"
   6.100    val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
   6.101    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_less_cancel_disj
   6.102 @@ -469,7 +469,7 @@
   6.103  
   6.104  structure LeCancelFactor = ExtractCommonTermFun
   6.105   (open CancelFactorCommon
   6.106 -  val prove_conv = Bin_Simprocs.prove_conv "nat_leq_cancel_factor"
   6.107 +  val prove_conv = Bin_Simprocs.prove_conv
   6.108    val mk_bal   = HOLogic.mk_binrel "op <="
   6.109    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
   6.110    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_le_cancel_disj
   6.111 @@ -477,7 +477,7 @@
   6.112  
   6.113  structure DivideCancelFactor = ExtractCommonTermFun
   6.114   (open CancelFactorCommon
   6.115 -  val prove_conv = Bin_Simprocs.prove_conv "nat_divide_cancel_factor"
   6.116 +  val prove_conv = Bin_Simprocs.prove_conv
   6.117    val mk_bal   = HOLogic.mk_binop "Divides.op div"
   6.118    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
   6.119    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
     7.1 --- a/src/HOL/Real/RealArith0.ML	Thu Aug 08 23:49:44 2002 +0200
     7.2 +++ b/src/HOL/Real/RealArith0.ML	Thu Aug 08 23:50:23 2002 +0200
     7.3 @@ -208,7 +208,7 @@
     7.4  
     7.5  structure DivCancelNumeralFactor = CancelNumeralFactorFun
     7.6   (open CancelNumeralFactorCommon
     7.7 -  val prove_conv = prove_conv "realdiv_cancel_numeral_factor"
     7.8 +  val prove_conv = Bin_Simprocs.prove_conv
     7.9    val mk_bal   = HOLogic.mk_binop "HOL.divide"
    7.10    val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
    7.11    val cancel = real_mult_div_cancel1 RS trans
    7.12 @@ -217,7 +217,7 @@
    7.13  
    7.14  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    7.15   (open CancelNumeralFactorCommon
    7.16 -  val prove_conv = prove_conv "realeq_cancel_numeral_factor"
    7.17 +  val prove_conv = Bin_Simprocs.prove_conv
    7.18    val mk_bal   = HOLogic.mk_eq
    7.19    val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
    7.20    val cancel = real_mult_eq_cancel1 RS trans
    7.21 @@ -226,7 +226,7 @@
    7.22  
    7.23  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    7.24   (open CancelNumeralFactorCommon
    7.25 -  val prove_conv = prove_conv "realless_cancel_numeral_factor"
    7.26 +  val prove_conv = Bin_Simprocs.prove_conv
    7.27    val mk_bal   = HOLogic.mk_binrel "op <"
    7.28    val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
    7.29    val cancel = real_mult_less_cancel1 RS trans
    7.30 @@ -235,7 +235,7 @@
    7.31  
    7.32  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    7.33   (open CancelNumeralFactorCommon
    7.34 -  val prove_conv = prove_conv "realle_cancel_numeral_factor"
    7.35 +  val prove_conv = Bin_Simprocs.prove_conv
    7.36    val mk_bal   = HOLogic.mk_binrel "op <="
    7.37    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
    7.38    val cancel = real_mult_le_cancel1 RS trans
    7.39 @@ -326,7 +326,7 @@
    7.40  
    7.41  structure EqCancelFactor = ExtractCommonTermFun
    7.42   (open CancelFactorCommon
    7.43 -  val prove_conv = prove_conv "real_eq_cancel_factor"
    7.44 +  val prove_conv = Bin_Simprocs.prove_conv
    7.45    val mk_bal   = HOLogic.mk_eq
    7.46    val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
    7.47    val simplify_meta_eq  = cancel_simplify_meta_eq real_mult_eq_cancel1
    7.48 @@ -335,7 +335,7 @@
    7.49  
    7.50  structure DivideCancelFactor = ExtractCommonTermFun
    7.51   (open CancelFactorCommon
    7.52 -  val prove_conv = prove_conv "real_divide_cancel_factor"
    7.53 +  val prove_conv = Bin_Simprocs.prove_conv
    7.54    val mk_bal   = HOLogic.mk_binop "HOL.divide"
    7.55    val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
    7.56    val simplify_meta_eq  = cancel_simplify_meta_eq real_mult_div_cancel_disj