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

author	nipkow
	Tue, 21 Dec 2010 08:38:03 +0100
changeset 41341	e65a122057ad
parent 35762	af3ff2ba4c54
permissions	-rw-r--r--