equal
deleted
inserted
replaced
27 [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, |
27 [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, |
28 rtac @{thm constrainsI} 1, |
28 rtac @{thm constrainsI} 1, |
29 full_simp_tac ss 1, |
29 full_simp_tac ss 1, |
30 REPEAT (FIRSTGOAL (etac disjE)), |
30 REPEAT (FIRSTGOAL (etac disjE)), |
31 ALLGOALS (clarify_tac cs), |
31 ALLGOALS (clarify_tac cs), |
32 ALLGOALS (asm_lr_simp_tac ss)]) i; |
32 ALLGOALS (asm_full_simp_tac ss)]) i; |
33 |
33 |
34 (*proves "ensures/leadsTo" properties when the program is specified*) |
34 (*proves "ensures/leadsTo" properties when the program is specified*) |
35 fun ensures_tac(cs,ss) sact = |
35 fun ensures_tac(cs,ss) sact = |
36 SELECT_GOAL |
36 SELECT_GOAL |
37 (EVERY [REPEAT (Always_Int_tac 1), |
37 (EVERY [REPEAT (Always_Int_tac 1), |