isabelle: src/HOL/UNITY/SubstAx.thy@95b619c7289b (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
5277 e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable" paulson parents: 5253 diff changeset	6	LeadsTo relation: restricted to the set of reachable states.
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	7	*)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	8
5313 1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union paulson parents: 5277 diff changeset	9	SubstAx = WFair + Constrains +
4776 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
5648 fe887910e32e specifications as sets of programs paulson parents: 5620 diff changeset	13	LeadsTo :: "['a set, 'a set] => 'a program set"
fe887910e32e specifications as sets of programs paulson parents: 5620 diff changeset	14	"LeadsTo A B == {F. F : leadsTo (reachable F Int A)
fe887910e32e specifications as sets of programs paulson parents: 5620 diff changeset	15	(reachable F Int B)}"
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	16	end

author	wenzelm
	Mon, 09 Nov 1998 15:34:23 +0100
changeset 5830	95b619c7289b
parent 5648	fe887910e32e
child 6536	281d44905cab
permissions	-rw-r--r--