--- a/src/HOL/Hyperreal/HyperArith0.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Hyperreal/HyperArith0.ML Thu Aug 08 23:50:23 2002 +0200
@@ -223,8 +223,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv
- "hyprealdiv_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
val cancel = hypreal_mult_div_cancel1 RS trans
@@ -233,8 +232,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv
- "hyprealeq_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
val cancel = hypreal_mult_eq_cancel1 RS trans
@@ -243,8 +241,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv
- "hyprealless_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" hyprealT
val cancel = hypreal_mult_less_cancel1 RS trans
@@ -253,8 +250,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv
- "hyprealle_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" hyprealT
val cancel = hypreal_mult_le_cancel1 RS trans
@@ -344,8 +340,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv
- "hypreal_eq_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_eq_cancel1
@@ -354,8 +349,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv
- "hypreal_divide_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT
val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj
--- a/src/HOL/Hyperreal/HyperBin.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML Thu Aug 08 23:50:23 2002 +0200
@@ -383,7 +383,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealeq_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" hyprealT
val bal_add1 = hypreal_eq_add_iff1 RS trans
@@ -392,7 +392,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealless_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" hyprealT
val bal_add1 = hypreal_less_add_iff1 RS trans
@@ -401,7 +401,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealle_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" hyprealT
val bal_add1 = hypreal_le_add_iff1 RS trans
@@ -435,8 +435,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val left_distrib = left_hypreal_add_mult_distrib RS trans
- val prove_conv = Real_Numeral_Simprocs.prove_conv_nohyps
- "hypreal_combine_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps
val trans_tac = Real_Numeral_Simprocs.trans_tac
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
@@ -483,8 +482,7 @@
val is_numeral = Bin_Simprocs.is_numeral
val numeral_0_eq_0 = hypreal_numeral_0_eq_0
val numeral_1_eq_1 = hypreal_numeral_1_eq_1
- val prove_conv = Real_Numeral_Simprocs.prove_conv_nohyps
- "hypreal_abstract_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
end
--- a/src/HOL/Integ/int_arith1.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu Aug 08 23:50:23 2002 +0200
@@ -225,7 +225,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
val bal_add1 = eq_add_iff1 RS trans
@@ -234,7 +234,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
val bal_add1 = less_add_iff1 RS trans
@@ -243,7 +243,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
val bal_add1 = le_add_iff1 RS trans
@@ -277,7 +277,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val left_distrib = left_zadd_zmult_distrib RS trans
- val prove_conv = Bin_Simprocs.prove_conv_nohyps "int_combine_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps
val trans_tac = trans_tac
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
--- a/src/HOL/Integ/int_factor_simprocs.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Thu Aug 08 23:50:23 2002 +0200
@@ -54,7 +54,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "intdiv_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
val cancel = int_mult_div_cancel1 RS trans
@@ -63,7 +63,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
val cancel = int_mult_eq_cancel1 RS trans
@@ -72,7 +72,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
val cancel = int_mult_less_cancel1 RS trans
@@ -81,7 +81,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
val cancel = int_mult_le_cancel1 RS trans
@@ -177,7 +177,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "int_eq_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_eq_cancel1
@@ -185,7 +185,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "int_divide_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
--- a/src/HOL/Integ/nat_bin.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Integ/nat_bin.ML Thu Aug 08 23:50:23 2002 +0200
@@ -229,7 +229,7 @@
val is_numeral = Bin_Simprocs.is_numeral
val numeral_0_eq_0 = numeral_0_eq_0
val numeral_1_eq_1 = numeral_1_eq_Suc_0
- val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_abstract_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
end
--- a/src/HOL/Integ/nat_simprocs.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Aug 08 23:50:23 2002 +0200
@@ -268,7 +268,7 @@
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "nateq_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val bal_add1 = nat_eq_add_iff1 RS trans
@@ -277,7 +277,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "natless_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
val bal_add1 = nat_less_add_iff1 RS trans
@@ -286,7 +286,7 @@
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "natle_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
val bal_add1 = nat_le_add_iff1 RS trans
@@ -295,7 +295,7 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
- val prove_conv = Bin_Simprocs.prove_conv "natdiff_cancel_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "op -"
val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
val bal_add1 = nat_diff_add_eq1 RS trans
@@ -337,7 +337,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val left_distrib = left_add_mult_distrib RS trans
- val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_combine_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps
val trans_tac = trans_tac
val norm_tac = ALLGOALS
(simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
@@ -371,7 +371,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "natdiv_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
val cancel = nat_mult_div_cancel1 RS trans
@@ -380,7 +380,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "nateq_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val cancel = nat_mult_eq_cancel1 RS trans
@@ -389,7 +389,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "natless_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
val cancel = nat_mult_less_cancel1 RS trans
@@ -398,7 +398,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "natle_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
val cancel = nat_mult_le_cancel1 RS trans
@@ -453,7 +453,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "nat_eq_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
@@ -461,7 +461,7 @@
structure LessCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "nat_less_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj
@@ -469,7 +469,7 @@
structure LeCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "nat_leq_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj
@@ -477,7 +477,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = Bin_Simprocs.prove_conv "nat_divide_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "Divides.op div"
val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj
--- a/src/HOL/Real/RealArith0.ML Thu Aug 08 23:49:44 2002 +0200
+++ b/src/HOL/Real/RealArith0.ML Thu Aug 08 23:50:23 2002 +0200
@@ -208,7 +208,7 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realdiv_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
val cancel = real_mult_div_cancel1 RS trans
@@ -217,7 +217,7 @@
structure EqCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realeq_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
val cancel = real_mult_eq_cancel1 RS trans
@@ -226,7 +226,7 @@
structure LessCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realless_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <"
val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
val cancel = real_mult_less_cancel1 RS trans
@@ -235,7 +235,7 @@
structure LeCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
- val prove_conv = prove_conv "realle_cancel_numeral_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel "op <="
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
val cancel = real_mult_le_cancel1 RS trans
@@ -326,7 +326,7 @@
structure EqCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = prove_conv "real_eq_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1
@@ -335,7 +335,7 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
- val prove_conv = prove_conv "real_divide_cancel_factor"
+ val prove_conv = Bin_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binop "HOL.divide"
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj