src/HOL/Auth/ROOT.ML
changeset 3121 cbb6c0c1c58a
parent 2530 02ccf78ad0a3
child 3207 fe79ad367d77
     1.1 --- a/src/HOL/Auth/ROOT.ML	Wed May 07 12:50:26 1997 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Wed May 07 13:01:43 1997 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4  proof_timing := true;
     1.5  goals_limit := 1;
     1.6  
     1.7 +(*New version of addss isn't ready--too slow*)
     1.8 +val op addss = op unsafe_addss;
     1.9 +
    1.10  (*Shared-key protocols*)
    1.11  time_use_thy "NS_Shared";
    1.12  time_use_thy "OtwayRees";