src/HOL/Auth/ROOT.ML
changeset 13508 890d736b93a5
parent 9000 c20d58286a51
child 13550 5a176b8dda84
     1.1 --- a/src/HOL/Auth/ROOT.ML	Sat Aug 17 14:55:08 2002 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Wed Aug 21 15:53:30 2002 +0200
     1.3 @@ -25,3 +25,11 @@
     1.4  time_use_thy "NS_Public_Bad";
     1.5  time_use_thy "NS_Public";
     1.6  time_use_thy "TLS";
     1.7 +
     1.8 +(*Blanqui's "guard" concept: protocol-independent secrecy*)
     1.9 +time_use_thy "Guard/P1";
    1.10 +time_use_thy "Guard/P2";
    1.11 +time_use_thy "Guard/NS_Public";
    1.12 +time_use_thy "Guard/OtwayRees";
    1.13 +time_use_thy "Guard/Yahalom";
    1.14 +time_use_thy "Guard/Proto";