Template:L guards

From Event-B
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