src/HOL/Auth/ROOT.ML

--- a/src/HOL/Auth/ROOT.ML	Sat Aug 17 14:55:08 2002 +0200
+++ b/src/HOL/Auth/ROOT.ML	Wed Aug 21 15:53:30 2002 +0200
@@ -25,3 +25,11 @@
 time_use_thy "NS_Public_Bad";
 time_use_thy "NS_Public";
 time_use_thy "TLS";
+
+(*Blanqui's "guard" concept: protocol-independent secrecy*)
+time_use_thy "Guard/P1";
+time_use_thy "Guard/P2";
+time_use_thy "Guard/NS_Public";
+time_use_thy "Guard/OtwayRees";
+time_use_thy "Guard/Yahalom";
+time_use_thy "Guard/Proto";