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

32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	1	(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4776 1f9362e769c1 New UNITY theory paulson parents: diff changeset	2	Copyright 1998 University of Cambridge
1f9362e769c1 New UNITY theory paulson parents: diff changeset	3	*)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	4
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	5	(Verifying security protocols using UNITY)
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 32624 diff changeset	6	no_document use_thys ["../Auth/Public"];
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	7
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 32624 diff changeset	8	use_thys [
41892 2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	9	(Basic meta-theory)
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	10	"UNITY_Main",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	11
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	12	(Simple examples: no composition)
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	13	"Simple/Deadlock",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	14	"Simple/Common",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	15	"Simple/Network",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	16	"Simple/Token",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	17	"Simple/Channel",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	18	"Simple/Lift",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	19	"Simple/Mutex",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	20	"Simple/Reach",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	21	"Simple/Reachability",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	22
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	23	(Verifying security protocols using UNITY)
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	24	"Simple/NSP_Bad",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	25
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	26	(Example of composition)
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	27	"Comp/Handshake",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	28
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	29	(Universal properties examples)
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	30	"Comp/Counter",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	31	"Comp/Counterc",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	32	"Comp/Priority",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	33
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	34	"Comp/TimerArray",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	35	"Comp/Progress",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	36
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	37	"Comp/Alloc",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	38	"Comp/AllocImpl",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	39	"Comp/Client",
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	40
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	41	(obsolete)
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473; wenzelm parents: 33615 diff changeset	42	"ELT"
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 32624 diff changeset	43	];

author	blanchet
	Sun, 06 Nov 2011 13:37:49 +0100
changeset 45368	ff2edf24e83a
parent 41892	2386fb64feaf
permissions	-rw-r--r--