isabelle: src/HOL/UNITY/SubstAx.thy@1861a564d7e2 (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
5253 82a5ca6290aa New record type of programs paulson parents: 5111 diff changeset	13	LeadsTo :: "['a program, 'a set, 'a set] => bool"
82a5ca6290aa New record type of programs paulson parents: 5111 diff changeset	14	"LeadsTo prg A B ==
82a5ca6290aa New record type of programs paulson parents: 5111 diff changeset	15	leadsTo (Acts prg)
82a5ca6290aa New record type of programs paulson parents: 5111 diff changeset	16	(reachable prg Int A)
82a5ca6290aa New record type of programs paulson parents: 5111 diff changeset	17	(reachable prg Int B)"
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	18	end

author	paulson
	Thu, 13 Aug 1998 18:06:40 +0200
changeset 5313	1861a564d7e2
parent 5277	e4297d03e5d2
child 5620	3ac11c4af76a
permissions	-rw-r--r--