isabelle: src/HOL/UNITY/ROOT.ML@29c346b165d4 (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
14203 97df98601d23 conversion of NSP_Bad to Isar script paulson parents: 13853 diff changeset	23	(Verifying security protocols using UNITY)
97df98601d23 conversion of NSP_Bad to Isar script paulson parents: 13853 diff changeset	24	with_path "../Auth" (no_document use_thy) "Public";
97df98601d23 conversion of NSP_Bad to Isar script paulson parents: 13853 diff changeset	25	with_path "../Auth" time_use_thy "Simple/NSP_Bad";
11193 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)
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	28	time_use_thy "Comp/Handshake";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	29
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	30	(Universal properties examples)
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	31	time_use_thy "Comp/Counter";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	32	time_use_thy "Comp/Counterc";
851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	33	time_use_thy "Comp/Priority";
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	34
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	35	time_use_thy "Comp/TimerArray";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	36
13790 8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13785 diff changeset	37	(Allocator example)
21633 d1cb78244e30 theory Alloc no longer works -- quick_and_dirty; wenzelm parents: 14203 diff changeset	38	(* FIXME some parts no longer work -- had been commented out for a long time *)
d1cb78244e30 theory Alloc no longer works -- quick_and_dirty; wenzelm parents: 14203 diff changeset	39	setmp quick_and_dirty true
d1cb78244e30 theory Alloc no longer works -- quick_and_dirty; wenzelm parents: 14203 diff changeset	40	time_use_thy "Comp/Alloc";
11193 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
	Wed, 06 Dec 2006 01:12:43 +0100
changeset 21672	29c346b165d4
parent 21633	d1cb78244e30
child 24147	edc90be09ac1
permissions	-rw-r--r--