isabelle: src/HOL/Auth/ROOT.ML@75d20f367e94 (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";
4449 df30e75f670f tuned; wenzelm parents: 3475 diff changeset	12	set proof_timing;
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)
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	16	time_use_thy "NS_Shared";
5053 75d20f367e94 New example Kerberos_BAN by G Bella paulson parents: 4449 diff changeset	17	time_use_thy "Kerberos_BAN";
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	18	time_use_thy "OtwayRees";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	19	time_use_thy "OtwayRees_AN";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	20	time_use_thy "OtwayRees_Bad";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	21	time_use_thy "WooLam";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	22	time_use_thy "Recur";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	23	time_use_thy "Yahalom";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	24	time_use_thy "Yahalom2";
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	25
2325 ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	26	(Public-key protocols)
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	27	time_use_thy "NS_Public_Bad";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	28	time_use_thy "NS_Public";
3475 368206f85f4b New theory TLS paulson parents: 3207 diff changeset	29	time_use_thy "TLS";
2325 ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	30

author	paulson
	Fri, 19 Jun 1998 10:34:33 +0200
changeset 5053	75d20f367e94
parent 4449	df30e75f670f
child 5359	bd539b72d484
permissions	-rw-r--r--