src/HOL/TLA/Memory/MIlive.ML
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 6255 db63752140c7
     1.1 --- a/src/HOL/TLA/Memory/MIlive.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MIlive.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -286,7 +286,7 @@
     1.4     "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& $(ImpInv rmhist p)) \
     1.5  \   .& SF(MClkReply memCh crCh cst p)_(c p) .& []<>($(S6 rmhist p))  \
     1.6  \   .-> []<>($(S1 rmhist p))"
     1.7 -   (fn _ => [Auto_tac(),
     1.8 +   (fn _ => [Auto_tac,
     1.9  	     subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1,
    1.10  	     eres_inst_tac [("P","<MClkReply memCh crCh cst p>_(c p)")]
    1.11  	                   EnsuresInfinite 1, atac 1,