isabelle: src/HOL/UNITY/SubstAx.thy@98a2afab3f86 (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
6536 281d44905cab made many specification operators infix paulson parents: 5648 diff changeset	6	Weak 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
6536 281d44905cab made many specification operators infix paulson parents: 5648 diff changeset	11	consts
281d44905cab made many specification operators infix paulson parents: 5648 diff changeset	12	LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	13
6536 281d44905cab made many specification operators infix paulson parents: 5648 diff changeset	14	defs
281d44905cab made many specification operators infix paulson parents: 5648 diff changeset	15	LeadsTo_def
6575 70d758762c50 new definitions of Co and LeadsTo paulson parents: 6536 diff changeset	16	"A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	17	end

author	paulson
	Thu, 26 Aug 1999 11:33:24 +0200
changeset 7359	98a2afab3f86
parent 6575	70d758762c50
child 8041	e3237d8c18d6
permissions	-rw-r--r--