isabelle: src/ZF/UNITY/ROOT.ML@1c14f77201d4 (annotated)

23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	1	(* Title: ZF/UNITY/ROOT.ML
11479 697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	2	ID: $Id$
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	5
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	6	ZF/UNITY proofs.
11479 697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	7	*)
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	8
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	9	use_thys [
039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	10	(Simple examples: no composition)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	11	"Mutex",
14052 e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety paulson parents: 14046 diff changeset	12
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	13	(Basic meta-theory)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	14	"Guar",
11479 697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	15
23912 039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	16	(Prefix relation; the Allocator example)
039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	17	"Distributor", "Merge", "ClientImpl", "AllocImpl"
039ae566a4a2 simultaneous use_thys; wenzelm parents: 14095 diff changeset	18	];

author	haftmann
	Mon, 20 Jul 2009 09:52:09 +0200
changeset 32078	1c14f77201d4
parent 23912	039ae566a4a2
child 35762	af3ff2ba4c54
permissions	-rw-r--r--