equal
deleted
inserted
replaced
77 (* comp *) |
77 (* comp *) |
78 by (best_tac (claset() addss (simpset())) 1); |
78 by (best_tac (claset() addss (simpset())) 1); |
79 (* while *) |
79 (* while *) |
80 by Safe_tac; |
80 by Safe_tac; |
81 by (ALLGOALS Asm_full_simp_tac); |
81 by (ALLGOALS Asm_full_simp_tac); |
82 by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]); |
82 by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]); |
83 by (rewtac Gamma_def); |
83 by (rewtac Gamma_def); |
84 by Safe_tac; |
84 by Safe_tac; |
85 by (EVERY1 [dtac bspec, atac]); |
85 by (EVERY1 [dtac bspec, atac]); |
86 by (ALLGOALS Asm_full_simp_tac); |
86 by (ALLGOALS Asm_full_simp_tac); |
87 (* while, if *) |
87 (* while, if *) |