isabelle: src/HOL/UNITY/UNITY_Examples.thy@b174d384293e (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
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	5	header {* Various examples for UNITY *}
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	6
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	7	theory UNITY_Examples
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	8	imports
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	9	UNITY_Main
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	10
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	11	(Simple examples: no composition)
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	12	"Simple/Deadlock"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	13	"Simple/Common"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	14	"Simple/Network"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	15	"Simple/Token"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	16	"Simple/Channel"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	17	"Simple/Lift"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	18	"Simple/Mutex"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	19	"Simple/Reach"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	20	"Simple/Reachability"
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	21
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	22	(Verifying security protocols using UNITY)
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	23	"Simple/NSP_Bad"
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	24
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	25	(Example of composition)
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	26	"Comp/Handshake"
10782 ddb433987557 new examples by Sidi Ehmety paulson parents: 10265 diff changeset	27
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	28	(Universal properties examples)
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	29	"Comp/Counter"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	30	"Comp/Counterc"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	31	"Comp/Priority"
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	32
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	33	"Comp/TimerArray"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	34	"Comp/Progress"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	35
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	36	"Comp/Alloc"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	37	"Comp/AllocImpl"
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	38	"Comp/Client"
24147 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"
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	42
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	43	begin
8987 718907f55f62 fixed the dependences paulson parents: 8334 diff changeset	44
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	45	end

author	blanchet
	Wed, 09 Dec 2009 12:26:42 +0100
changeset 34042	b174d384293e
parent 32624	3dec57ec3473
permissions	-rw-r--r--