isabelle: src/HOL/Auth/ROOT.ML@3ad2493fa0e0 (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;
2123 959f791b6f0f Two new protocol variants paulson parents: 2091 diff changeset	13	goals_limit := 1;
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	14
2325 ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	15	(Shared-key protocols)
1971 30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	16	use_thy "NS_Shared";
30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	17	use_thy "OtwayRees";
2091 644104f85d14 Addition of OtwayRees_AN paulson parents: 1995 diff changeset	18	use_thy "OtwayRees_AN";
2123 959f791b6f0f Two new protocol variants paulson parents: 2091 diff changeset	19	use_thy "OtwayRees_Bad";
2274 1b1b46adc9b3 Addition of Woo-Lam protocol paulson parents: 2123 diff changeset	20	use_thy "WooLam";
2450 3ad2493fa0e0 Addition of Auth/Recur paulson parents: 2325 diff changeset	21	use_thy "Recur";
1995 c80e58e78d9c Addition of Yahalom protocol paulson parents: 1971 diff changeset	22	use_thy "Yahalom";
2123 959f791b6f0f Two new protocol variants paulson parents: 2091 diff changeset	23	use_thy "Yahalom2";
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	24
2325 ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	25	(Public-key protocols)
ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	26	use_thy "NS_Public_Bad";
ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	27	use_thy "NS_Public";
ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	28

author	paulson
	Thu, 19 Dec 1996 11:54:19 +0100
changeset 2450	3ad2493fa0e0
parent 2325	ea8a1fc512e6
child 2530	02ccf78ad0a3
permissions	-rw-r--r--