Template:L guards
From Event-B
Revision as of 14:12, 26 February 2009 by imported>Mathieu (New page: <noinclude> ==Usage== Template use to typeset an event name in an event-b listing. ==Example== {{l_events}} {{l_event|control|extended|ordinary}} {{l_parameters}} {{l_param|a}} {{l_param|...)
Usage
Template use to typeset an event name in an event-b listing.
Example
EVENTS
control ≙
// extended and ordinary
ANY
a
x
WHERE
grd1 :
x ⊆ next
WITH
y :
{{{2}}}
THEN
act1 :
pro :∈ BOOL
END
END
Template
WHERE