src/HOL/Integ/int_factor_simprocs.ML
changeset 13485 acf39e924091
parent 13462 56610e2ba220
child 14113 7b3513ba0f86
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Aug 08 23:49:44 2002 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Aug 08 23:50:23 2002 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  structure DivCancelNumeralFactor = CancelNumeralFactorFun
     1.6   (open CancelNumeralFactorCommon
     1.7 -  val prove_conv = Bin_Simprocs.prove_conv "intdiv_cancel_numeral_factor"
     1.8 +  val prove_conv = Bin_Simprocs.prove_conv
     1.9    val mk_bal   = HOLogic.mk_binop "Divides.op div"
    1.10    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    1.11    val cancel = int_mult_div_cancel1 RS trans
    1.12 @@ -63,7 +63,7 @@
    1.13  
    1.14  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    1.15   (open CancelNumeralFactorCommon
    1.16 -  val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numeral_factor"
    1.17 +  val prove_conv = Bin_Simprocs.prove_conv
    1.18    val mk_bal   = HOLogic.mk_eq
    1.19    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.20    val cancel = int_mult_eq_cancel1 RS trans
    1.21 @@ -72,7 +72,7 @@
    1.22  
    1.23  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    1.24   (open CancelNumeralFactorCommon
    1.25 -  val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numeral_factor"
    1.26 +  val prove_conv = Bin_Simprocs.prove_conv
    1.27    val mk_bal   = HOLogic.mk_binrel "op <"
    1.28    val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    1.29    val cancel = int_mult_less_cancel1 RS trans
    1.30 @@ -81,7 +81,7 @@
    1.31  
    1.32  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    1.33   (open CancelNumeralFactorCommon
    1.34 -  val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numeral_factor"
    1.35 +  val prove_conv = Bin_Simprocs.prove_conv
    1.36    val mk_bal   = HOLogic.mk_binrel "op <="
    1.37    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    1.38    val cancel = int_mult_le_cancel1 RS trans
    1.39 @@ -177,7 +177,7 @@
    1.40  
    1.41  structure EqCancelFactor = ExtractCommonTermFun
    1.42   (open CancelFactorCommon
    1.43 -  val prove_conv = Bin_Simprocs.prove_conv "int_eq_cancel_factor"
    1.44 +  val prove_conv = Bin_Simprocs.prove_conv
    1.45    val mk_bal   = HOLogic.mk_eq
    1.46    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.47    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
    1.48 @@ -185,7 +185,7 @@
    1.49  
    1.50  structure DivideCancelFactor = ExtractCommonTermFun
    1.51   (open CancelFactorCommon
    1.52 -  val prove_conv = Bin_Simprocs.prove_conv "int_divide_cancel_factor"
    1.53 +  val prove_conv = Bin_Simprocs.prove_conv
    1.54    val mk_bal   = HOLogic.mk_binop "Divides.op div"
    1.55    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    1.56    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj