src/HOL/UNITY/SubstAx.thy

proper symbol markup with \isamath, \isatext;
support sub/super scripts:

(*  Title:      HOL/UNITY/SubstAx
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Weak LeadsTo relation (restricted to the set of reachable states)
*)

SubstAx = WFair + Constrains + 

constdefs
   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
    "A Ensures B == {F. F : (reachable F Int A) ensures B}"

   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"

syntax (xsymbols)
  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)

end