isabelle: src/HOL/UNITY/SubstAx.thy@66925577cefe (annotated)

4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	1	(* Title: HOL/UNITY/SubstAx
1f9362e769c1 New UNITY theory paulson parents: diff changeset	2	ID: $Id$
1f9362e769c1 New UNITY theory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
1f9362e769c1 New UNITY theory paulson parents: diff changeset	5
1f9362e769c1 New UNITY theory paulson parents: diff changeset	6	My treatment of the Substitution Axiom -- not as an axiom!
1f9362e769c1 New UNITY theory paulson parents: diff changeset	7	*)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	8
1f9362e769c1 New UNITY theory paulson parents: diff changeset	9	SubstAx = WFair +
1f9362e769c1 New UNITY theory paulson parents: diff changeset	10
1f9362e769c1 New UNITY theory paulson parents: diff changeset	11	constdefs
1f9362e769c1 New UNITY theory paulson parents: diff changeset	12
5111 8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 4776 diff changeset	13	LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool"
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 4776 diff changeset	14	"LeadsTo == %(Init,Acts) A B.
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 4776 diff changeset	15	leadsTo Acts (reachable (Init,Acts) Int A)
8f4b72f0c15d Uncurried functions LeadsTo and reach paulson parents: 4776 diff changeset	16	(reachable (Init,Acts) Int B)"
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	17
1f9362e769c1 New UNITY theory paulson parents: diff changeset	18
1f9362e769c1 New UNITY theory paulson parents: diff changeset	19	end

author	wenzelm
	Fri, 31 Jul 1998 11:03:31 +0200
changeset 5228	66925577cefe
parent 5111	8f4b72f0c15d
child 5253	82a5ca6290aa
permissions	-rw-r--r--