src/HOL/Integ/int_arith1.ML
changeset 9544 f9202e219a29
parent 9436 62bb04ab4b01
child 9571 c869d1886a32
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Aug 07 10:26:02 2000 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Aug 07 10:27:11 2000 +0200
     1.3 @@ -178,7 +178,7 @@
     1.4  fun trans_tac None      = all_tac
     1.5    | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
     1.6  
     1.7 -fun prove_conv name tacs sg (t, u) =
     1.8 +fun prove_conv name tacs sg (hyps: thm list) (t,u) =
     1.9    if t aconv u then None
    1.10    else
    1.11    let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
    1.12 @@ -189,6 +189,9 @@
    1.13  	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
    1.14    end;
    1.15  
    1.16 +(*version without the hyps argument*)
    1.17 +fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
    1.18 +
    1.19  fun simplify_meta_eq rules =
    1.20      mk_meta_eq o
    1.21      simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
    1.22 @@ -268,7 +271,7 @@
    1.23    val mk_coeff		= mk_coeff
    1.24    val dest_coeff	= dest_coeff 1
    1.25    val left_distrib	= left_zadd_zmult_distrib RS trans
    1.26 -  val prove_conv	= prove_conv "int_combine_numerals"
    1.27 +  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
    1.28    val trans_tac          = trans_tac
    1.29    val norm_tac = ALLGOALS
    1.30                     (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@