# HG changeset patch
# User wenzelm
# Date 1028843423 -7200
# Node ID acf39e92409128a00c9f2712b2dea0d00008a11b
# Parent  d8f5d339176605007c4076a6c38e318797e656cf
tuned prove_conv (error reporting done within meta_simplifier.ML);

diff -r d8f5d3391766 -r acf39e924091 src/HOL/Hyperreal/HyperArith0.ML
--- 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
diff -r d8f5d3391766 -r acf39e924091 src/HOL/Hyperreal/HyperBin.ML
--- 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
diff -r d8f5d3391766 -r acf39e924091 src/HOL/Integ/int_arith1.ML
--- 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@
diff -r d8f5d3391766 -r acf39e924091 src/HOL/Integ/int_factor_simprocs.ML
--- 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
diff -r d8f5d3391766 -r acf39e924091 src/HOL/Integ/nat_bin.ML
--- 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
diff -r d8f5d3391766 -r acf39e924091 src/HOL/Integ/nat_simprocs.ML
--- 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
diff -r d8f5d3391766 -r acf39e924091 src/HOL/Real/RealArith0.ML
--- 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