diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -86,7 +86,7 @@
 by simp
 
 abbreviation
-  not_MPair :: "msg => bool"
+  not_MPair :: "msg => bool" where
   "not_MPair X == ~ is_MPair X"
 
 lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P"
@@ -370,7 +370,7 @@
    ))"
 
 abbreviation
-  spies' :: "event list => msg set"
+  spies' :: "event list => msg set" where
   "spies' == knows' Spy"
 
 subsubsection{*decomposition of knows into knows' and initState*}
@@ -452,7 +452,7 @@
 "knows_max A evs == knows_max' A evs Un initState A"
 
 abbreviation
-  spies_max :: "event list => msg set"
+  spies_max :: "event list => msg set" where
   "spies_max evs == knows_max Spy evs"
 
 subsubsection{*basic facts about @{term knows_max}*}