src/HOL/UNITY/SubstAx.thy
author paulson
Thu Apr 29 10:51:58 1999 +0200 (1999-04-29)
changeset 6536 281d44905cab
parent 5648 fe887910e32e
child 6575 70d758762c50
permissions -rw-r--r--
made many specification operators infix
paulson@4776
     1
(*  Title:      HOL/UNITY/SubstAx
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@6536
     6
Weak LeadsTo relation (restricted to the set of reachable states)
paulson@4776
     7
*)
paulson@4776
     8
paulson@5313
     9
SubstAx = WFair + Constrains + 
paulson@4776
    10
paulson@6536
    11
consts
paulson@6536
    12
   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson@4776
    13
paulson@6536
    14
defs
paulson@6536
    15
   LeadsTo_def
paulson@6536
    16
    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
paulson@6536
    17
	   	            (reachable F  Int  B)}"
paulson@4776
    18
end