isabelle: src/HOL/UNITY/ROOT.ML@cc8245843abc (annotated)

4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	1	(* Title: HOL/UNITY/ROOT
1f9362e769c1 New UNITY theory paulson parents: diff changeset	2	ID: $Id$
1f9362e769c1 New UNITY theory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
1f9362e769c1 New UNITY theory paulson parents: diff changeset	5
1f9362e769c1 New UNITY theory paulson parents: diff changeset	6	Root file for UNITY proofs.
1f9362e769c1 New UNITY theory paulson parents: diff changeset	7	*)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	8
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	9	(Basic meta-theory)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	10	time_use_thy "FP";
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	11	time_use_thy "WFair";
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	12
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	13	(Simple examples: no composition)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	14	time_use_thy "Simple/Deadlock";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	15	time_use_thy "Simple/Common";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	16	time_use_thy "Simple/Network";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	17	time_use_thy "Simple/Token";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	18	time_use_thy "Simple/Channel";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	19	time_use_thy "Simple/Lift";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	20	time_use_thy "Simple/Mutex";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	21	time_use_thy "Simple/Reach";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	22	time_use_thy "Simple/Reachability";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	23
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	24	with_path "../Auth" (to find Public.thy)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	25	time_use_thy"Simple/NSP_Bad";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	26
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	27	(Example of composition)
5620 3ac11c4af76a tidying and renaming paulson parents: 5430 diff changeset	28	time_use_thy "Comp";
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	29	time_use_thy "Comp/Handshake";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	30
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	31	(Universal properties examples)
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	32	time_use_thy "Comp/Counter";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	33	time_use_thy "Comp/Counterc";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	34	time_use_thy "Comp/Priority";
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	35
6730 fa1f63249077 new theories Follows and ListOrder paulson parents: 6536 diff changeset	36	(Allocator example)
6295 351b3c2b0d83 removed the infernal States, eqStates, compatible, etc. paulson parents: 6216 diff changeset	37	time_use_thy "PPROD";
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	38	time_use_thy "Comp/TimerArray";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	39
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	40	time_use_thy "Comp/Alloc";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	41	time_use_thy "Comp/AllocImpl";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	42	time_use_thy "Comp/Client";
8987 718907f55f62 fixed the dependences paulson parents: 8334 diff changeset	43
718907f55f62 fixed the dependences paulson parents: 8334 diff changeset	44	time_use_thy "ELT"; (obsolete)

author	wenzelm
	Tue, 16 Jul 2002 18:41:50 +0200
changeset 13377	cc8245843abc
parent 11193	851c90b23a9e
child 13785	e2fcd88be55d
permissions	-rw-r--r--