IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-pre-init-ma-single-pre-compatible a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top,
d1:x:Id fp-> Type, P1:Top.
ds || d1 a = a1 (with ds: ds (init: init action a:T aprecondition a(v) is
aP) ||+ (with ds: d1 aaction a1:T1 aprecondition a1(v) is
aP1 s v)
By:
ProveBaseCompatTac
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top,
a = a1
