src/HOL/Auth/ROOT.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9000 c20d58286a51
child 13508 890d736b93a5
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
2123
959f791b6f0f Two new protocol variants
paulson
parents: 2091
diff changeset
     9
goals_limit := 1;
1944
ea0f573b222b ROOT file for Auth directory
paulson
parents:
diff changeset
    10
2325
ea8a1fc512e6 Loads new public-key examples
paulson
parents: 2274
diff changeset
    11
(*Shared-key protocols*)
2530
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    12
time_use_thy "NS_Shared";
5053
75d20f367e94 New example Kerberos_BAN by G Bella
paulson
parents: 4449
diff changeset
    13
time_use_thy "Kerberos_BAN";
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents: 6400
diff changeset
    14
time_use_thy "KerberosIV";
2530
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    15
time_use_thy "OtwayRees";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    16
time_use_thy "OtwayRees_AN";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    17
time_use_thy "OtwayRees_Bad";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    18
time_use_thy "WooLam";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    19
time_use_thy "Recur";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    20
time_use_thy "Yahalom";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    21
time_use_thy "Yahalom2";
6400
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 6349
diff changeset
    22
time_use_thy "Yahalom_Bad";
1944
ea0f573b222b ROOT file for Auth directory
paulson
parents:
diff changeset
    23
2325
ea8a1fc512e6 Loads new public-key examples
paulson
parents: 2274
diff changeset
    24
(*Public-key protocols*)
2530
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    25
time_use_thy "NS_Public_Bad";
02ccf78ad0a3 Now requests runtimes of all theories
paulson
parents: 2450
diff changeset
    26
time_use_thy "NS_Public";
3475
368206f85f4b New theory TLS
paulson
parents: 3207
diff changeset
    27
time_use_thy "TLS";