--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Jul 02 12:10:58 2020 +0000
@@ -981,7 +981,8 @@
from fvar obtain upd w
where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
v: "v=(w,upd)"
- by (cases "fvar statDeclC stat fn a s2") simp
+ by (cases "fvar statDeclC stat fn a s2")
+ (simp, use surjective_pairing in blast)
{
fix j val fix s::state
assume "normal s3"
@@ -1025,7 +1026,8 @@
from avar obtain upd w
where upd: "upd = snd (fst (avar G i a s2))" and
v: "v=(w,upd)"
- by (cases "avar G i a s2") simp
+ by (cases "avar G i a s2")
+ (simp, use surjective_pairing in blast)
{
fix j val fix s::state
assume "normal s2'"