equal
deleted
inserted
replaced
97 by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1); |
97 by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1); |
98 by Auto_tac; |
98 by Auto_tac; |
99 (*Resulting state \\<in> n=1, p=false, m=4, u=false. |
99 (*Resulting state \\<in> n=1, p=false, m=4, u=false. |
100 Execution of V1 (the command of process v guarded by n=1) sets p:=true, |
100 Execution of V1 (the command of process v guarded by n=1) sets p:=true, |
101 violating the invariant!*) |
101 violating the invariant!*) |
102 (*Check that subgoals remain \\<in> proof failed.*) |
102 (*Check that subgoals remain: proof failed.*) |
103 getgoal 1; |
103 getgoal 1; |
104 |
104 |
105 |
105 |
106 (*** Progress for U ***) |
106 (*** Progress for U ***) |
107 |
107 |