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|...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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