isabelle: src/HOL/UNITY/ROOT.ML@7d8e0a47392e (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
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	9	(Verifying security protocols using UNITY)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	10	no_document use_thy "../Auth/Public";
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	11
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	12	use_thys [
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	13	(Basic meta-theory)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	14	"UNITY_Main",
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	15
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	16	(Simple examples: no composition)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	17	"Simple/Deadlock",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	18	"Simple/Common",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	19	"Simple/Network",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	20	"Simple/Token",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	21	"Simple/Channel",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	22	"Simple/Lift",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	23	"Simple/Mutex",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	24	"Simple/Reach",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	25	"Simple/Reachability",
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	26
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	27	(Verifying security protocols using UNITY)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	28	"Simple/NSP_Bad",
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	29
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	30	(Example of composition)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	31	"Comp/Handshake",
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	32
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	33	(Universal properties examples)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	34	"Comp/Counter",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	35	"Comp/Counterc",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	36	"Comp/Priority",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	37
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	38	"Comp/TimerArray",
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	39
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	40	(obsolete)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	41	"ELT"
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	42	];
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	43
13790 8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13785 diff changeset	44	(Allocator example)
21633 d1cb78244e30 theory Alloc no longer works -- quick_and_dirty; wenzelm parents: 14203 diff changeset	45	(* 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	46	setmp quick_and_dirty true
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	47	use_thy "Comp/Alloc";
8987 718907f55f62 fixed the dependences paulson parents: 8334 diff changeset	48
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	49	use_thys ["Comp/AllocImpl", "Comp/Client"];

author	wenzelm
	Wed, 03 Oct 2007 00:02:56 +0200
changeset 24819	7d8e0a47392e
parent 24147	edc90be09ac1
child 28529	7ff939586e83
permissions	-rw-r--r--