isabelle: src/ZF/UNITY/ROOT.ML@3ef76d545aaf (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	wenzelm
	Tue, 31 Jul 2012 19:55:04 +0200
changeset 48627	3ef76d545aaf
parent 35762	af3ff2ba4c54
permissions	-rw-r--r--