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

11479 697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	1	(* Title: ZF/UNITY/ROOT
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
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	6	Root file for ZF/UNITY proofs.
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	7	*)
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	8
14046 6616e6c53d48 updating ZF-UNITY with Sidi's new material paulson parents: 12198 diff changeset	9	add_path "../Induct"; (for Multisets)
6616e6c53d48 updating ZF-UNITY with Sidi's new material paulson parents: 12198 diff changeset	10
14052 e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety paulson parents: 14046 diff changeset	11	(Simple examples: no composition)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety paulson parents: 14046 diff changeset	12	time_use_thy"Mutex";
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety paulson parents: 14046 diff changeset	13
11479 697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	14	(Basic meta-theory)
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	15	time_use_thy "Guar";
697dcaaf478f new ZF/UNITY theory paulson parents: diff changeset	16
14095 a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new paulson parents: 14060 diff changeset	17	(* Prefix relation; the Allocator example *)
14052 e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety paulson parents: 14046 diff changeset	18	time_use_thy "Distributor";
14053 4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl paulson parents: 14052 diff changeset	19	time_use_thy "Merge";
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl paulson parents: 14052 diff changeset	20	time_use_thy "ClientImpl";
14060 c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas paulson parents: 14053 diff changeset	21	time_use_thy "AllocImpl";

author	wenzelm
	Wed, 13 Jul 2005 16:07:36 +0200
changeset 16814	b829a6c9a87a
parent 14095	a1ba833d6b61
child 23912	039ae566a4a2
permissions	-rw-r--r--