src/ZF/arith_data.ML
changeset 13126 97e83120d6c8
parent 12206 60d52181840c
child 13155 dcbf6cb95534
     1.1 --- a/src/ZF/arith_data.ML	Thu May 09 17:50:59 2002 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Thu May 09 17:51:19 2002 +0200
     1.3 @@ -146,7 +146,8 @@
     1.4    val dest_coeff        = dest_coeff
     1.5    val find_first_coeff  = find_first_coeff []
     1.6    val norm_tac_ss1 = ZF_ss addsimps add_0s@add_succs@mult_1s@add_ac
     1.7 -  val norm_tac_ss2 = ZF_ss addsimps add_ac@mult_ac@tc_rules@natifys
     1.8 +  val norm_tac_ss2 = ZF_ss addsimps add_0s@mult_1s@
     1.9 +                                    add_ac@mult_ac@tc_rules@natifys
    1.10    val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
    1.11                   THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
    1.12    val numeral_simp_tac_ss = ZF_ss addsimps add_0s@tc_rules@natifys
    1.13 @@ -254,6 +255,7 @@
    1.14  test "x : nat --> x #+ y = x";
    1.15  test "x : nat ==> x #+ y < x";
    1.16  test "x : nat ==> x < y#+x";
    1.17 +test "x : nat ==> x le succ(x)";
    1.18  
    1.19  (*fails: no typing information isn't visible*)
    1.20  test "x #+ y = x";