src/HOL/Auth/ROOT.ML
changeset 3207 fe79ad367d77
parent 3121 cbb6c0c1c58a
child 3475 368206f85f4b
     1.1 --- a/src/HOL/Auth/ROOT.ML	Thu May 15 15:51:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Thu May 15 15:51:47 1997 +0200
     1.3 @@ -12,9 +12,6 @@
     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";