src/ZF/arith_data.ML
changeset 35409 5c5bb83f2bae
parent 35408 b48ab741683b
child 38513 33ab01218ae1
     1.1 --- a/src/ZF/arith_data.ML	Sat Feb 27 23:13:01 2010 +0100
     1.2 +++ b/src/ZF/arith_data.ML	Sun Feb 28 22:30:51 2010 +0100
     1.3 @@ -163,9 +163,9 @@
     1.4    val prove_conv = prove_conv "nateq_cancel_numerals"
     1.5    val mk_bal   = FOLogic.mk_eq
     1.6    val dest_bal = FOLogic.dest_eq
     1.7 -  val bal_add1 = @{thm eq_add_iff} RS iff_trans
     1.8 -  val bal_add2 = @{thm eq_add_iff} RS iff_trans
     1.9 -  fun trans_tac _ = gen_trans_tac iff_trans
    1.10 +  val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
    1.11 +  val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
    1.12 +  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
    1.13    end;
    1.14  
    1.15  structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
    1.16 @@ -176,9 +176,9 @@
    1.17    val prove_conv = prove_conv "natless_cancel_numerals"
    1.18    val mk_bal   = FOLogic.mk_binrel "Ordinal.lt"
    1.19    val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
    1.20 -  val bal_add1 = @{thm less_add_iff} RS iff_trans
    1.21 -  val bal_add2 = @{thm less_add_iff} RS iff_trans
    1.22 -  fun trans_tac _ = gen_trans_tac iff_trans
    1.23 +  val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
    1.24 +  val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
    1.25 +  fun trans_tac _ = gen_trans_tac @{thm iff_trans}
    1.26    end;
    1.27  
    1.28  structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
    1.29 @@ -189,9 +189,9 @@
    1.30    val prove_conv = prove_conv "natdiff_cancel_numerals"
    1.31    val mk_bal   = FOLogic.mk_binop "Arith.diff"
    1.32    val dest_bal = FOLogic.dest_bin "Arith.diff" iT
    1.33 -  val bal_add1 = @{thm diff_add_eq} RS trans
    1.34 -  val bal_add2 = @{thm diff_add_eq} RS trans
    1.35 -  fun trans_tac _ = gen_trans_tac trans
    1.36 +  val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
    1.37 +  val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
    1.38 +  fun trans_tac _ = gen_trans_tac @{thm trans}
    1.39    end;
    1.40  
    1.41  structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);