isabelle: src/HOL/UNITY/ROOT.ML@f478d5a9d238 (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 [
261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 32624 diff changeset	9	"UNITY_Main", (Basic meta-theory)
261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 32624 diff changeset	10	"UNITY_Examples" (Examples)
261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 32624 diff changeset	11	];
9112 44fc37919579 added the AllocImpl example paulson parents: 9000 diff changeset	12