equal
deleted
inserted
replaced
10 by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1); |
10 by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1); |
11 qed "not_zless_zless1_eq"; |
11 qed "not_zless_zless1_eq"; |
12 |
12 |
13 |
13 |
14 (*split_all_tac causes a big blow-up*) |
14 (*split_all_tac causes a big blow-up*) |
15 claset_ref() := claset() delSWrapper "split_all_tac"; |
15 claset_ref() := claset() delSWrapper "record_split_tac"; |
16 |
16 |
17 Delsimps [split_paired_All]; |
17 Delsimps [split_paired_All]; |
18 |
18 |
19 Goal "[| x ~: A; y : A |] ==> x ~= y"; |
19 Goal "[| x ~: A; y : A |] ==> x ~= y"; |
20 by (Blast_tac 1); |
20 by (Blast_tac 1); |