--- a/src/HOL/Auth/Yahalom.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML Sat Feb 15 17:52:31 1997 +0100
@@ -16,6 +16,8 @@
HOL_quantifiers := false;
Pretty.setdepth 25;
+val op addss = op unsafe_addss;
+
(*A "possibility property": there are traces that reach the end*)
goal thy