equal
deleted
inserted
replaced
1297 case (Jmp j) |
1297 case (Jmp j) |
1298 thus ?case |
1298 thus ?case |
1299 apply - |
1299 apply - |
1300 apply (rule MGFn_NormalI) |
1300 apply (rule MGFn_NormalI) |
1301 apply (rule ax_derivs.Jmp [THEN conseq1]) |
1301 apply (rule ax_derivs.Jmp [THEN conseq1]) |
1302 apply (auto intro: eval.Jmp simp add: abupd_def2) |
1302 apply (auto intro: eval.Jmp) |
1303 done |
1303 done |
1304 next |
1304 next |
1305 case (Throw e) |
1305 case (Throw e) |
1306 thus ?case |
1306 thus ?case |
1307 apply - |
1307 apply - |