src/HOL/Auth/ROOT.ML
author wenzelm
Fri, 19 Dec 1997 10:28:33 +0100
changeset 4449 df30e75f670f
parent 3475 368206f85f4b
child 5053 75d20f367e94
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
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";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    17
time_use_thy "OtwayRees";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    18
time_use_thy "OtwayRees_AN";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    19
time_use_thy "OtwayRees_Bad";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    20
time_use_thy "WooLam";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    21
time_use_thy "Recur";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    22
time_use_thy "Yahalom";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    23
time_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*)
2530
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    26
time_use_thy "NS_Public_Bad";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    27
time_use_thy "NS_Public";
3475
368206f85f4b New theory TLS
paulson
parents: 3207
diff changeset
    28
time_use_thy "TLS";
2325
ea8a1fc512e6 Loads new public-key examples
paulson
parents: 2274
diff changeset
    29