isabelle: src/HOL/UNITY/ROOT.ML@95d51043d2a3 (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)
13785 e2fcd88be55d Partial conversion of UNITY to Isar new-style theories paulson parents: 11193 diff changeset	10	time_use_thy "UNITY_Main";
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	11
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	12	(Simple examples: no composition)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	13	time_use_thy "Simple/Deadlock";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	14	time_use_thy "Simple/Common";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	15	time_use_thy "Simple/Network";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	16	time_use_thy "Simple/Token";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	17	time_use_thy "Simple/Channel";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	18	time_use_thy "Simple/Lift";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	19	time_use_thy "Simple/Mutex";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	20	time_use_thy "Simple/Reach";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	21	time_use_thy "Simple/Reachability";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	22
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	23	with_path "../Auth" (to find Public.thy)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	24	time_use_thy"Simple/NSP_Bad";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	25
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	26	(Example of composition)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	27	time_use_thy "Comp/Handshake";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	28
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	29	(Universal properties examples)
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	30	time_use_thy "Comp/Counter";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	31	time_use_thy "Comp/Counterc";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	32	time_use_thy "Comp/Priority";
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	33
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	34	time_use_thy "Comp/TimerArray";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	35
13790 8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13785 diff changeset	36	(Allocator example)
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	37	time_use_thy "Comp/Alloc";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	38	time_use_thy "Comp/AllocImpl";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	39	time_use_thy "Comp/Client";
8987 718907f55f62 fixed the dependences paulson parents: 8334 diff changeset	40
718907f55f62 fixed the dependences paulson parents: 8334 diff changeset	41	time_use_thy "ELT"; (obsolete)

author	paulson
	Tue, 15 Jul 2003 15:12:22 +0200
changeset 14112	95d51043d2a3
parent 13853	89131afa9f01
child 14203	97df98601d23
permissions	-rw-r--r--