IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
trigger1 wf loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id.
A T x = "trigger" locl(a) = k trigger1(loc;T;A;P;i;k;a;x) MsgA List
By:
Unfold `trigger1` 0 THEN MaAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html