isabelle: src/HOL/UNITY/SubstAx.thy@82a5ca6290aa (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
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
	Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253	82a5ca6290aa
parent 5111	8f4b72f0c15d
child 5277	e4297d03e5d2
permissions	-rw-r--r--