equal
deleted
inserted
replaced
41 by (Asm_simp_tac 1); |
41 by (Asm_simp_tac 1); |
42 qed "PREC_Suc"; |
42 qed "PREC_Suc"; |
43 |
43 |
44 Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; |
44 Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; |
45 |
45 |
46 |
|
47 Addsimps ack.rules; |
|
48 |
46 |
49 (*PROPERTY A 4*) |
47 (*PROPERTY A 4*) |
50 Goal "j < ack(i,j)"; |
48 Goal "j < ack(i,j)"; |
51 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
49 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
52 by (ALLGOALS Asm_simp_tac); |
50 by (ALLGOALS Asm_simp_tac); |