isabelle: src/HOL/UNITY/ROOT.ML@362f59fe5092 (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	*)
1f9362e769c1 New UNITY theory paulson parents: diff changeset	5
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	6	(Verifying security protocols using UNITY)
edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21633 diff changeset	7	no_document use_thy "../Auth/Public";
11193 851c90b23a9e reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp paulson parents: 10782 diff changeset	8
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	9	(Basic meta-theory)
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	10	use_thy "UNITY_Main";
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	11
32624 3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	12	(Examples)
3dec57ec3473 entry point theory for examples; reactivated half-dead example haftmann parents: 28866 diff changeset	13	use_thy "UNITY_Examples";

author	wenzelm
	Thu, 22 Oct 2009 15:50:12 +0200
changeset 33071	362f59fe5092
parent 32624	3dec57ec3473
child 33615	261abc2e3155
permissions	-rw-r--r--