isabelle: src/ZF/UNITY/ROOT.ML@f745bcc4a1e5 (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
	Mon, 27 Feb 2012 16:56:25 +0100
changeset 46711	f745bcc4a1e5
parent 35762	af3ff2ba4c54
permissions	-rw-r--r--