equal
deleted
inserted
replaced
35 |
35 |
36 (* Arithmetic *) |
36 (* Arithmetic *) |
37 |
37 |
38 goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; |
38 goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; |
39 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
39 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
40 by (Blast_tac 1); |
|
41 qed "pred_suc"; |
40 qed "pred_suc"; |
42 |
41 |
43 |
42 |
44 Addsimps (hd_append :: set_lemmas); |
43 Addsimps (hd_append :: set_lemmas); |