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
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@4776
     6
My treatment of the Substitution Axiom -- not as an axiom!
paulson@4776
     7
*)
paulson@4776
     8
paulson@4776
     9
SubstAx = WFair +
paulson@4776
    10
paulson@4776
    11
constdefs
paulson@4776
    12
paulson@5111
    13
   LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool"
paulson@5111
    14
    "LeadsTo == %(Init,Acts) A B.
paulson@5111
    15
		 leadsTo Acts (reachable (Init,Acts) Int A)
paulson@5111
    16
			      (reachable (Init,Acts) Int B)"
paulson@4776
    17
paulson@4776
    18
paulson@4776
    19
end