src/HOL/UNITY/SubstAx.thy
author paulson
Thu Jul 02 16:53:55 1998 +0200 (1998-07-02)
changeset 5111 8f4b72f0c15d
parent 4776 1f9362e769c1
child 5253 82a5ca6290aa
permissions -rw-r--r--
Uncurried functions LeadsTo and reach
Deleted leading parameters thanks to new Goal command
     1 (*  Title:      HOL/UNITY/SubstAx
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 My treatment of the Substitution Axiom -- not as an axiom!
     7 *)
     8 
     9 SubstAx = WFair +
    10 
    11 constdefs
    12 
    13    LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool"
    14     "LeadsTo == %(Init,Acts) A B.
    15 		 leadsTo Acts (reachable (Init,Acts) Int A)
    16 			      (reachable (Init,Acts) Int B)"
    17 
    18 
    19 end