equal
deleted
inserted
replaced
85 by (strip_tac 1); |
85 by (strip_tac 1); |
86 by (rtac mp 1); |
86 by (rtac mp 1); |
87 by (assume_tac 2); |
87 by (assume_tac 2); |
88 by (etac induct2 1); |
88 by (etac induct2 1); |
89 by (fast_tac (claset() addSIs [monoI]) 1); |
89 by (fast_tac (claset() addSIs [monoI]) 1); |
90 by (stac gfp_Tarski 1); |
90 by (stac gfp_unfold 1); |
91 by (fast_tac (claset() addSIs [monoI]) 1); |
91 by (fast_tac (claset() addSIs [monoI]) 1); |
92 by (Fast_tac 1); |
92 by (Fast_tac 1); |
93 qed "wp_While"; |
93 qed "wp_While"; |
94 |
94 |
95 Delsimps [C_while]; |
95 Delsimps [C_while]; |