changeset 1342 | f6651b6b0482 |
parent 1328 | 9a449a91425d |
child 1465 | 5d7a7e439cec |
1341:69fec018854c | 1342:f6651b6b0482 |
---|---|
115 |
115 |
116 by(Asm_full_simp_tac 1); |
116 by(Asm_full_simp_tac 1); |
117 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
117 by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); |
118 |
118 |
119 by(Asm_full_simp_tac 1); |
119 by(Asm_full_simp_tac 1); |
120 result(); |
120 qed"ntp_correct"; |