src/HOL/UNITY/SubstAx.thy
author paulson
Thu Oct 15 11:35:07 1998 +0200 (1998-10-15)
changeset 5648 fe887910e32e
parent 5620 3ac11c4af76a
child 6536 281d44905cab
permissions -rw-r--r--
specifications as sets of programs
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@5277
     6
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@4776
    11
constdefs
paulson@4776
    12
paulson@5648
    13
   LeadsTo :: "['a set, 'a set] => 'a program set"
paulson@5648
    14
    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
paulson@5648
    15
	   	                    (reachable F  Int  B)}"
paulson@4776
    16
end