
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -85,9 +85,9 @@
 lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)"
 by simp
 
-syntax not_MPair :: "msg => bool"
-
-translations "not_MPair X" == "~ is_MPair X"
+abbreviation
+  not_MPair :: "msg => bool"
+  "not_MPair X == ~ is_MPair X"
 
 lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P"
 by auto
@@ -369,11 +369,9 @@
      | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
    ))"
 
-translations "spies" == "knows Spy"
-
-syntax spies' :: "event list => msg set"
-
-translations "spies'" == "knows' Spy"
+abbreviation
+  spies' :: "event list => msg set"
+  "spies' == knows' Spy"
 
 subsubsection{*decomposition of knows into knows' and initState*}
 
@@ -453,9 +451,9 @@
 constdefs knows_max :: "agent => event list => msg set"
 "knows_max A evs == knows_max' A evs Un initState A"
 
-consts spies_max :: "event list => msg set"
-
-translations "spies_max evs" == "knows_max Spy evs"
+abbreviation
+  spies_max :: "event list => msg set"
+  "spies_max evs == knows_max Spy evs"
 
 subsubsection{*basic facts about @{term knows_max}*}
 




