Now requests runtimes of all theories
authorpaulson
Mon, 20 Jan 1997 10:27:45 +0100
changeset 2530 02ccf78ad0a3
parent 2529 e40ca839758d
child 2531 7cfa1a9c744d
Now requests runtimes of all theories
src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Mon Jan 20 10:20:58 1997 +0100
+++ b/src/HOL/Auth/ROOT.ML	Mon Jan 20 10:27:45 1997 +0100
@@ -13,16 +13,16 @@
 goals_limit := 1;
 
 (*Shared-key protocols*)
-use_thy "NS_Shared";
-use_thy "OtwayRees";
-use_thy "OtwayRees_AN";
-use_thy "OtwayRees_Bad";
-use_thy "WooLam";
-use_thy "Recur";
-use_thy "Yahalom";
-use_thy "Yahalom2";
+time_use_thy "NS_Shared";
+time_use_thy "OtwayRees";
+time_use_thy "OtwayRees_AN";
+time_use_thy "OtwayRees_Bad";
+time_use_thy "WooLam";
+time_use_thy "Recur";
+time_use_thy "Yahalom";
+time_use_thy "Yahalom2";
 
 (*Public-key protocols*)
-use_thy "NS_Public_Bad";
-use_thy "NS_Public";
+time_use_thy "NS_Public_Bad";
+time_use_thy "NS_Public";