equal
deleted
inserted
replaced
128 with G Load app show ?thesis |
128 with G Load app show ?thesis |
129 by (cases s2) (auto simp add: sup_state_conv dest: sup_loc_some) |
129 by (cases s2) (auto simp add: sup_state_conv dest: sup_loc_some) |
130 next |
130 next |
131 case Store |
131 case Store |
132 with G app show ?thesis |
132 with G app show ?thesis |
133 by (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 sup_state_conv) |
133 by (cases s2, auto simp add: sup_loc_Cons2 sup_state_conv) |
134 next |
134 next |
135 case LitPush |
135 case LitPush |
136 with G app show ?thesis by (cases s2, auto simp add: sup_state_conv) |
136 with G app show ?thesis by (cases s2, auto simp add: sup_state_conv) |
137 next |
137 next |
138 case New |
138 case New |