src/HOL/Auth/ROOT.ML
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3475 368206f85f4b
child 4449 df30e75f670f
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
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";
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*)
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