# HG changeset patch
# User paulson
# Date 965636831 -7200
# Node ID f9202e219a295c0b01a510fcf3f532d36fb102b0
# Parent  ce61d1c1a509f3850ff7818f1419ce7d13fc1578
added a dummy "thm list" argument to prove_conv for the new interface to
Cancel_Numerals

diff -r ce61d1c1a509 -r f9202e219a29 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Mon Aug 07 10:26:02 2000 +0200
+++ b/src/HOL/Integ/IntDef.ML	Mon Aug 07 10:27:11 2000 +0200
@@ -232,8 +232,6 @@
 qed "zadd_assoc_swap";
 
 
-(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
-
 (**** zmult: multiplication on Integ ****)
 
 (*Congruence property for multiplication*)
@@ -302,7 +300,7 @@
                         add_ac @ mult_ac) 1);
 qed "zadd_zmult_distrib";
 
-val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
+val zmult_commute'= inst "z" "w" zmult_commute;
 
 Goal "w * (- z) = - (w * (z::int))";
 by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
diff -r ce61d1c1a509 -r f9202e219a29 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Mon Aug 07 10:26:02 2000 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon Aug 07 10:27:11 2000 +0200
@@ -178,7 +178,7 @@
 fun trans_tac None      = all_tac
   | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
 
-fun prove_conv name tacs sg (t, u) =
+fun prove_conv name tacs sg (hyps: thm list) (t,u) =
   if t aconv u then None
   else
   let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
@@ -189,6 +189,9 @@
 	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   end;
 
+(*version without the hyps argument*)
+fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
+
 fun simplify_meta_eq rules =
     mk_meta_eq o
     simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
@@ -268,7 +271,7 @@
   val mk_coeff		= mk_coeff
   val dest_coeff	= dest_coeff 1
   val left_distrib	= left_zadd_zmult_distrib RS trans
-  val prove_conv	= prove_conv "int_combine_numerals"
+  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   val trans_tac          = trans_tac
   val norm_tac = ALLGOALS
                    (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
diff -r ce61d1c1a509 -r f9202e219a29 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Mon Aug 07 10:26:02 2000 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon Aug 07 10:27:11 2000 +0200
@@ -143,9 +143,9 @@
       handle TERM _ => [t];
 
 (*DON'T do the obvious simplifications; that would create special cases*)
-fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
+fun mk_coeff (k,t) = mk_times (mk_numeral k, t);
 
-(*Express t as a product of (possibly) a numeral with other sorted terms*)
+(*Express t as a product of (possibly) a numeral with other factors, sorted*)
 fun dest_coeff t =
     let val ts = sort Term.term_ord (dest_prod t)
         val (n, _, ts') = find_first_numeral [] ts
@@ -259,7 +259,8 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val left_distrib      = left_add_mult_distrib RS trans
-  val prove_conv        = prove_conv "nat_combine_numerals"
+  val prove_conv = 
+       Int_Numeral_Simprocs.prove_conv_nohyps "nat_combine_numerals"
   val trans_tac          = trans_tac
   val norm_tac = ALLGOALS
                    (simp_tac (HOL_ss addsimps add_0s@mult_1s@
diff -r ce61d1c1a509 -r f9202e219a29 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Mon Aug 07 10:26:02 2000 +0200
+++ b/src/HOL/Real/RealBin.ML	Mon Aug 07 10:27:11 2000 +0200
@@ -367,7 +367,7 @@
 fun trans_tac None      = all_tac
   | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
 
-fun prove_conv name tacs sg (t, u) =
+fun prove_conv name tacs sg (hyps: thm list) (t,u) =
   if t aconv u then None
   else
   let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
@@ -378,6 +378,9 @@
 	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   end;
 
+(*version without the hyps argument*)
+fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
+
 (*Final simplification: cancel + and *  *)
 val simplify_meta_eq = 
     Int_Numeral_Simprocs.simplify_meta_eq
@@ -459,7 +462,7 @@
   val mk_coeff		= mk_coeff
   val dest_coeff	= dest_coeff 1
   val left_distrib	= left_real_add_mult_distrib RS trans
-  val prove_conv	= prove_conv "real_combine_numerals"
+  val prove_conv	= prove_conv_nohyps "real_combine_numerals"
   val trans_tac          = trans_tac
   val norm_tac = ALLGOALS
                    (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@