src/HOL/Auth/Yahalom2.ML
changeset 2637 e9b203f854ae
parent 2516 4d68fbe6378b
child 3121 cbb6c0c1c58a
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Sat Feb 15 17:48:19 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Sat Feb 15 17:52:31 1997 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4  proof_timing:=true;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 +val op addss = op unsafe_addss;
     1.8  
     1.9  (*A "possibility property": there are traces that reach the end*)
    1.10  goal thy