isabelle: src/HOL/Auth/ROOT.ML@7e118eb32bdc (annotated)

1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	1	(* Title: HOL/Auth/ROOT
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	2	ID: $Id$
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	4	Copyright 1996 University of Cambridge
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	5
1971 30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	6	Root file for protocol proofs.
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	7	*)
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	8
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	10
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	11	writeln"Root file for HOL/Auth";
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	12	proof_timing := true;
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	13
1971 30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	14	use_thy "Shared";
30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	15	use_thy "NS_Shared";
30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	16	use_thy "OtwayRees";
2091 644104f85d14 Addition of OtwayRees_AN paulson parents: 1995 diff changeset	17	use_thy "OtwayRees_AN";
1995 c80e58e78d9c Addition of Yahalom protocol paulson parents: 1971 diff changeset	18	use_thy "Yahalom";
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	19

author	paulson
	Thu, 24 Oct 1996 10:30:43 +0200
changeset 2121	7e118eb32bdc
parent 2091	644104f85d14
child 2123	959f791b6f0f
permissions	-rw-r--r--