# HG changeset patch
# User wenzelm
# Date 1159479755 -7200
# Node ID 1d478c2d621fea5710792af8b08de060af311195
# Parent  9bc632ae588f3dd00a833a88bab056a51792a6e1
replaced syntax/translations by abbreviation;

diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -7,13 +7,12 @@
 
 theory CertifiedEmail imports Public begin
 
-syntax
-  TTP        :: agent
-  RPwd       :: "agent => key"
+abbreviation
+  TTP :: agent
+  "TTP == Server"
 
-translations
-  "TTP"   == "Server "
-  "RPwd"  == "shrK "
+  RPwd :: "agent => key"
+  "RPwd == shrK"
 
  
 (*FIXME: the four options should be represented by pairs of 0 or 1.
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -27,11 +27,10 @@
 
 
 text{*The constant "spies" is retained for compatibility's sake*}
-syntax
+
+abbreviation (input)
   spies  :: "event list => msg set"
-
-translations
-  "spies"   => "knows Spy"
+  "spies == knows Spy"
 
 text{*Spy has access to his own key for spoof messages, but Server is secure*}
 specification (bad)
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}*}
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -162,9 +162,9 @@
 
 subsection{*set obtained by decrypting a message*}
 
-syntax decrypt :: "msg set => key => msg => msg set"
-
-translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
+abbreviation (input)
+  decrypt :: "msg set => key => msg => msg set"
+  "decrypt H K Y == insert Y (H - {Crypt K Y})"
 
 lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |]
 ==> Nonce n:analz (decrypt H K Y)"
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -158,9 +158,9 @@
 
 subsection{*set obtained by decrypting a message*}
 
-syntax decrypt :: "msg set => key => msg => msg set"
-
-translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
+abbreviation (input)
+  decrypt :: "msg set => key => msg => msg set"
+  "decrypt H K Y == insert Y (H - {Crypt K Y})"
 
 lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
 ==> Key n:analz (decrypt H K Y)"
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/Guard_NS_Public.thy
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -17,28 +17,22 @@
 
 subsection{*messages used in the protocol*}
 
-syntax ns1 :: "agent => agent => nat => event"
-
-translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+abbreviation (input)
+  ns1 :: "agent => agent => nat => event"
+  "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
 
-syntax ns1' :: "agent => agent => agent => nat => event"
-
-translations "ns1' A' A B NA"
-=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
-
-syntax ns2 :: "agent => agent => nat => nat => event"
+  ns1' :: "agent => agent => agent => nat => event"
+  "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
 
-translations "ns2 B A NA NB"
-=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
-
-syntax ns2' :: "agent => agent => agent => nat => nat => event"
+  ns2 :: "agent => agent => nat => nat => event"
+  "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
 
-translations "ns2' B' B A NA NB"
-=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+  ns2' :: "agent => agent => agent => nat => nat => event"
+  "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
 
-syntax ns3 :: "agent => agent => nat => event"
+  ns3 :: "agent => agent => nat => event"
+  "ns3 A B NB == Says A B (Crypt (pubK B) (Nonce NB))"
 
-translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
 
 subsection{*definition of the protocol*}
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/Guard_OtwayRees.thy
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -15,53 +15,42 @@
 
 subsection{*messages used in the protocol*}
 
-syntax nil :: "msg"
-
-translations "nil" == "Number 0"
-
-syntax or1 :: "agent => agent => nat => event"
-
-translations "or1 A B NA"
-=> "Says A B {|Nonce NA, Agent A, Agent B,
-               Ciph A {|Nonce NA, Agent A, Agent B|}|}"
+abbreviation
+  nil :: "msg"
+  "nil == Number 0"
 
-syntax or1' :: "agent => agent => agent => nat => msg => event"
-
-translations "or1' A' A B NA X"
-=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
+  or1 :: "agent => agent => nat => event"
+  "or1 A B NA ==
+    Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
 
-syntax or2 :: "agent => agent => nat => nat => msg => event"
+  or1' :: "agent => agent => agent => nat => msg => event"
+  "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
 
-translations "or2 A B NA NB X"
-=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
+  or2 :: "agent => agent => nat => nat => msg => event"
+  "or2 A B NA NB X ==
+    Says B Server {|Nonce NA, Agent A, Agent B, X,
                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
 
-syntax or2' :: "agent => agent => agent => nat => nat => event"
-
-translations "or2' B' A B NA NB"
-=> "Says B' Server {|Nonce NA, Agent A, Agent B,
+  or2' :: "agent => agent => agent => nat => nat => event"
+  "or2' B' A B NA NB ==
+    Says B' Server {|Nonce NA, Agent A, Agent B,
                      Ciph A {|Nonce NA, Agent A, Agent B|},
                      Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
 
-syntax or3 :: "agent => agent => nat => nat => key => event"
-
-translations "or3 A B NA NB K"
-=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
+  or3 :: "agent => agent => nat => nat => key => event"
+  "or3 A B NA NB K ==
+    Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
                     Ciph B {|Nonce NB, Key K|}|}"
 
-syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
-
-translations "or3' S Y A B NA NB K"
-=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
-
-syntax or4 :: "agent => agent => nat => msg => event"
+  or3':: "agent => msg => agent => agent => nat => nat => key => event"
+  "or3' S Y A B NA NB K ==
+    Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
 
-translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
+  or4 :: "agent => agent => nat => msg => event"
+  "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
 
-syntax or4' :: "agent => agent => nat => msg => event"
-
-translations "or4' B' A NA K" =>
-"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
+  or4' :: "agent => agent => nat => key => event"
+  "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
 
 subsection{*definition of the protocol*}
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/Guard_Yahalom.thy
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -15,42 +15,34 @@
 
 subsection{*messages used in the protocol*}
 
-syntax ya1 :: "agent => agent => nat => event"
-
-translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
+abbreviation (input)
+  ya1 :: "agent => agent => nat => event"
+  "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
 
-syntax ya1' :: "agent => agent => agent => nat => event"
-
-translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
-
-syntax ya2 :: "agent => agent => nat => nat => event"
+  ya1' :: "agent => agent => agent => nat => event"
+  "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
 
-translations "ya2 A B NA NB"
-=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
-
-syntax ya2' :: "agent => agent => agent => nat => nat => event"
+  ya2 :: "agent => agent => nat => nat => event"
+  "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
 
-translations "ya2' B' A B NA NB"
-=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+  ya2' :: "agent => agent => agent => nat => nat => event"
+  "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
 
-syntax ya3 :: "agent => agent => nat => nat => key => event"
-
-translations "ya3 A B NA NB K"
-=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
+  ya3 :: "agent => agent => nat => nat => key => event"
+  "ya3 A B NA NB K ==
+    Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
                     Ciph B {|Agent A, Key K|}|}"
 
-syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
-
-translations "ya3' S Y A B NA NB K"
-=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
+  ya3':: "agent => msg => agent => agent => nat => nat => key => event"
+  "ya3' S Y A B NA NB K ==
+    Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
 
-syntax ya4 :: "agent => agent => nat => nat => msg => event"
-
-translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
+  ya4 :: "agent => agent => nat => nat => msg => event"
+  "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
 
-syntax ya4' :: "agent => agent => nat => nat => msg => event"
+  ya4' :: "agent => agent => nat => nat => msg => event"
+  "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
 
-translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
 
 subsection{*definition of the protocol*}
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/List_Msg.thy
--- a/src/HOL/Auth/Guard/List_Msg.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/List_Msg.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -17,15 +17,15 @@
 
 subsubsection{*nil is represented by any message which is not a pair*}
 
-syntax cons :: "msg => msg => msg"
-
-translations "cons x l" => "{|x,l|}"
+abbreviation (input)
+  cons :: "msg => msg => msg"
+  "cons x l == {|x,l|}"
 
 subsubsection{*induction principle*}
 
 lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |]
 ==> P l"
-by (induct l, auto)
+by (induct l) auto
 
 subsubsection{*head*}
 
@@ -50,7 +50,7 @@
 "len other = 0"
 
 lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
-by (cases l, auto)
+by (cases l) auto
 
 subsubsection{*membership*}
 
@@ -69,10 +69,10 @@
 "del (x, other) = other"
 
 lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
-by (induct l, auto)
+by (induct l) auto
 
 lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)"
-by (induct l, auto)
+by (induct l) auto
 
 subsubsection{*concatenation*}
 
@@ -83,7 +83,7 @@
 "app (other, l') = l'"
 
 lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
-by (induct l, auto)
+by (induct l) auto
 
 subsubsection{*replacement*}
 
@@ -104,7 +104,7 @@
 "ith (other, i) = other"
 
 lemma ith_head: "0 < len l ==> ith (l,0) = head l"
-by (cases l, auto)
+by (cases l) auto
 
 subsubsection{*insertion*}
 
@@ -115,7 +115,7 @@
 "ins (l, 0, y) = cons y l"
 
 lemma ins_head [simp]: "ins (l,0,y) = cons y l"
-by (cases l, auto)
+by (cases l) auto
 
 subsubsection{*truncation*}
 
@@ -126,16 +126,16 @@
 "trunc (cons x l, Suc i) = trunc (l,i)"
 
 lemma trunc_zero [simp]: "trunc (l,0) = l"
-by (cases l, auto)
+by (cases l) auto
 
 
 subsection{*Agent Lists*}
 
 subsubsection{*set of well-formed agent-list messages*}
 
-syntax nil :: msg
-
-translations "nil" == "Number 0"
+abbreviation
+  nil :: msg
+  "nil == Number 0"
 
 consts agl :: "msg set"
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -17,9 +17,9 @@
 
 types rule = "event set * event"
 
-syntax msg' :: "rule => msg"
-
-translations "msg' R" == "msg (snd R)"
+abbreviation
+  msg' :: "rule => msg"
+  "msg' R == msg (snd R)"
 
 types proto = "rule set"
 
@@ -76,17 +76,18 @@
 "ap s (Gets A X) = Gets (agent s A) (apm s X)"
 "ap s (Notes A X) = Notes (agent s A) (apm s X)"
 
-syntax
-ap' :: "rule => msg"
-apm' :: "rule => msg"
-priK' :: "subs => agent => key"
-pubK' :: "subs => agent => key"
+abbreviation
+  ap' :: "subs => rule => event"
+  "ap' s R == ap s (snd R)"
 
-translations
-"ap' s R" == "ap s (snd R)"
-"apm' s R" == "apm s (msg' R)"
-"priK' s A" == "priK (agent s A)"
-"pubK' s A" == "pubK (agent s A)"
+  apm' :: "subs => rule => msg"
+  "apm' s R == apm s (msg' R)"
+
+  priK' :: "subs => agent => key"
+  "priK' s A == priK (agent s A)"
+
+  pubK' :: "subs => agent => key"
+  "pubK' s A == pubK (agent s A)"
 
 subsection{*nonces generated by a rule*}
 
@@ -377,32 +378,31 @@
 
 consts
 ns :: proto
-ns1 :: rule
-ns2 :: rule
-ns3 :: rule
 
-translations
-"ns1" == "({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
+abbreviation
+  ns1 :: rule
+  "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
 
-"ns2" == "({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
-Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
+  ns2 :: rule
+  "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
+    Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
 
-"ns3" == "({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
-Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
-Says a b (Crypt (pubK b) (Nonce Nb)))"
+  ns3 :: rule
+  "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
+    Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
+    Says a b (Crypt (pubK b) (Nonce Nb)))"
 
 inductive ns intros
 [iff]: "ns1:ns"
 [iff]: "ns2:ns"
 [iff]: "ns3:ns"
 
-syntax
-ns3a :: msg
-ns3b :: msg
+abbreviation (input)
+  ns3a :: event
+  "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
 
-translations
-"ns3a" => "Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
-"ns3b" => "Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
+  ns3b :: event
+  "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
 
 constdefs keys :: "keyfun"
 "keys R' s' n evs == {priK' s' a, priK' s' b}"
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -10,33 +10,18 @@
 
 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
 
-syntax
+abbreviation
   Kas :: agent
-  Tgs :: agent  --{*the two servers are translations...*}
+  "Kas == Server"
 
-
-translations
-  "Kas"       == "Server "
-  "Tgs"       == "Friend 0"
+  Tgs :: agent
+  "Tgs == Friend 0"
 
 
 axioms
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
-(*The current time is the length of the trace*)
-syntax
-    CT :: "event list=>nat"
-
-    expiredAK :: "[nat, event list] => bool"
-
-    expiredSK :: "[nat, event list] => bool"
-
-    expiredA :: "[nat, event list] => bool"
-
-    valid :: "[nat, nat] => bool" ("valid _ wrt _")
-
-
 constdefs
  (* authKeys are those contained in an authTicket *)
     authKeys :: "event list => key set"
@@ -92,16 +77,22 @@
   replylife_LB [iff]: "Suc 0 \<le> replylife"
     by blast
 
-translations
-   "CT" == "length "
+abbreviation
+  (*The current time is the length of the trace*)
+  CT :: "event list=>nat"
+  "CT == length"
 
-   "expiredAK Ta evs" == "authKlife + Ta < CT evs"
+  expiredAK :: "[nat, event list] => bool"
+  "expiredAK Ta evs == authKlife + Ta < CT evs"
 
-   "expiredSK Ts evs" == "servKlife + Ts < CT evs"
+  expiredSK :: "[nat, event list] => bool"
+  "expiredSK Ts evs == servKlife + Ts < CT evs"
 
-   "expiredA T evs" == "authlife + T < CT evs"
+  expiredA :: "[nat, event list] => bool"
+  "expiredA T evs == authlife + T < CT evs"
 
-   "valid T1 wrt T2" == "T1 <= replylife + T2"
+  valid :: "[nat, nat] => bool" ("valid _ wrt _")
+  "valid T1 wrt T2 == T1 <= replylife + T2"
 
 (*---------------------------------------------------------------------*)
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/KerberosIV_Gets.thy
--- a/src/HOL/Auth/KerberosIV_Gets.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/KerberosIV_Gets.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -10,33 +10,18 @@
 
 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
 
-syntax
+abbreviation
   Kas :: agent
-  Tgs :: agent  --{*the two servers are translations...*}
+  "Kas == Server"
 
-
-translations
-  "Kas"       == "Server "
-  "Tgs"       == "Friend 0"
+  Tgs :: agent
+  "Tgs == Friend 0"
 
 
 axioms
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
-(*The current time is just the length of the trace!*)
-syntax
-    CT :: "event list=>nat"
-
-    expiredAK :: "[nat, event list] => bool"
-
-    expiredSK :: "[nat, event list] => bool"
-
-    expiredA :: "[nat, event list] => bool"
-
-    valid :: "[nat, nat] => bool" ("valid _ wrt _")
-
-
 constdefs
  (* authKeys are those contained in an authTicket *)
     authKeys :: "event list => key set"
@@ -80,16 +65,22 @@
   replylife_LB [iff]: "Suc 0 \<le> replylife"
     by blast
 
-translations
-   "CT" == "length "
+abbreviation
+  (*The current time is just the length of the trace!*)
+  CT :: "event list=>nat"
+  "CT == length"
 
-   "expiredAK Ta evs" == "authKlife + Ta < CT evs"
+  expiredAK :: "[nat, event list] => bool"
+  "expiredAK Ta evs == authKlife + Ta < CT evs"
 
-   "expiredSK Ts evs" == "servKlife + Ts < CT evs"
+  expiredSK :: "[nat, event list] => bool"
+  "expiredSK Ts evs == servKlife + Ts < CT evs"
 
-   "expiredA T evs" == "authlife + T < CT evs"
+  expiredA :: "[nat, event list] => bool"
+  "expiredA T evs == authlife + T < CT evs"
 
-   "valid T1 wrt T2" == "T1 <= replylife + T2"
+  valid :: "[nat, nat] => bool" ("valid _ wrt _")
+  "valid T1 wrt T2 == T1 <= replylife + T2"
 
 (*---------------------------------------------------------------------*)
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/KerberosV.thy
--- a/src/HOL/Auth/KerberosV.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/KerberosV.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -8,33 +8,18 @@
 
 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
 
-syntax
+abbreviation
   Kas :: agent
-  Tgs :: agent  --{*the two servers are translations...*}
+  "Kas == Server"
 
-
-translations
-  "Kas"       == "Server "
-  "Tgs"       == "Friend 0"
+  Tgs :: agent
+  "Tgs == Friend 0"
 
 
 axioms
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
-(*The current time is just the length of the trace!*)
-syntax
-    CT :: "event list=>nat"
-
-    expiredAK :: "[nat, event list] => bool"
-
-    expiredSK :: "[nat, event list] => bool"
-
-    expiredA :: "[nat, event list] => bool"
-
-    valid :: "[nat, nat] => bool"  ("valid _ wrt _")
-
-
 constdefs
  (* authKeys are those contained in an authTicket *)
     authKeys :: "event list => key set"
@@ -81,16 +66,22 @@
   replylife_LB [iff]: "Suc 0 \<le> replylife"
     by blast
 
-translations
-   "CT" == "length "
+abbreviation
+  (*The current time is just the length of the trace!*)
+  CT :: "event list=>nat"
+  "CT == length"
 
-   "expiredAK T evs" == "authKlife + T < CT evs"
+  expiredAK :: "[nat, event list] => bool"
+  "expiredAK T evs == authKlife + T < CT evs"
 
-   "expiredSK T evs" == "servKlife + T < CT evs"
+  expiredSK :: "[nat, event list] => bool"
+  "expiredSK T evs == servKlife + T < CT evs"
 
-   "expiredA T evs" == "authlife + T < CT evs"
+  expiredA :: "[nat, event list] => bool"
+  "expiredA T evs == authlife + T < CT evs"
 
-   "valid T1 wrt T2" == "T1 <= replylife + T2"
+  valid :: "[nat, nat] => bool"  ("valid _ wrt _")
+  "valid T1 wrt T2 == T1 <= replylife + T2"
 
 (*---------------------------------------------------------------------*)
 
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -20,11 +20,6 @@
 (* Temporal model of accidents: session keys can be leaked
                                 ONLY when they have expired *)
 
-syntax
-    CT :: "event list=>nat"
-    expiredK :: "[nat, event list] => bool"
-    expiredA :: "[nat, event list] => bool"
-
 consts
 
     (*Duration of the session key*)
@@ -43,13 +38,15 @@
   authlife_LB [iff]:    "0 < authlife"
     by blast
 
-
-translations
-   "CT" == "length "
+abbreviation
+  CT :: "event list=>nat"
+  "CT == length "
 
-   "expiredK T evs" == "sesKlife + T < CT evs"
+  expiredK :: "[nat, event list] => bool"
+  "expiredK T evs == sesKlife + T < CT evs"
 
-   "expiredA T evs" == "authlife + T < CT evs"
+  expiredA :: "[nat, event list] => bool"
+  "expiredA T evs == authlife + T < CT evs"
 
 
 constdefs
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Kerberos_BAN_Gets.thy
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -18,11 +18,6 @@
 (* Temporal modelization: session keys can be leaked
                           ONLY when they have expired *)
 
-syntax
-    CT :: "event list=>nat"
-    expiredK :: "[nat, event list] => bool"
-    expiredA :: "[nat, event list] => bool"
-
 consts
 
     (*Duration of the session key*)
@@ -44,12 +39,15 @@
     by blast
 
 
-translations
-   "CT" == "length "
+abbreviation
+  CT :: "event list=>nat"
+  "CT == length"
 
-   "expiredK T evs" == "sesKlife + T < CT evs"
+  expiredK :: "[nat, event list] => bool"
+  "expiredK T evs == sesKlife + T < CT evs"
 
-   "expiredA T evs" == "authlife + T < CT evs"
+  expiredA :: "[nat, event list] => bool"
+  "expiredA T evs == authlife + T < CT evs"
 
 
 constdefs
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Public.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -20,33 +20,32 @@
 consts
   publicKey :: "[keymode,agent] => key"
 
-syntax
+abbreviation
   pubEK :: "agent => key"
-  pubSK :: "agent => key"
+  "pubEK == publicKey Encryption"
 
-  privateKey :: "[bool,agent] => key"
-  priEK :: "agent => key"
-  priSK :: "agent => key"
+  pubSK :: "agent => key"
+  "pubSK == publicKey Signature"
 
-translations
-  "pubEK"  == "publicKey Encryption"
-  "pubSK"  == "publicKey Signature"
+  privateKey :: "[keymode, agent] => key"
+  "privateKey b A == invKey (publicKey b A)"
 
   (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
-  "privateKey b A" == "invKey (publicKey b A)"
-  "priEK A"  == "privateKey Encryption A"
-  "priSK A"  == "privateKey Signature A"
+  priEK :: "agent => key"
+  "priEK A == privateKey Encryption A"
+  priSK :: "agent => key"
+  "priSK A == privateKey Signature A"
 
 
-text{*These translations give backward compatibility.  They represent the
+text{*These abbreviations give backward compatibility.  They represent the
 simple situation where the signature and encryption keys are the same.*}
-syntax
+
+abbreviation
   pubK :: "agent => key"
+  "pubK A == pubEK A"
+
   priK :: "agent => key"
-
-translations
-  "pubK A" == "pubEK A"
-  "priK A" == "invKey (pubEK A)"
+  "priK A == invKey (pubEK A)"
 
 
 text{*By freeness of agents, no two agents have the same key.  Since
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Recur.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -9,8 +9,9 @@
 theory Recur imports Public begin
 
 text{*End marker for message bundles*}
-syntax        END :: "msg"
-translations "END" == "Number 0"
+abbreviation
+  END :: "msg"
+  "END == Number 0"
 
 (*Two session keys are distributed to each agent except for the initiator,
         who receives one.
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/Smartcard/EventSC.thy
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -24,10 +24,9 @@
  cloned  :: "card set"   (* cloned smart cards*)
  secureM :: "bool"(*assumption of secure means between agents and their cards*)
 
-syntax
+abbreviation
   insecureM :: bool (*certain protocols make no assumption of secure means*)
-translations
-  "insecureM" == "\<not>secureM"
+  "insecureM == \<not>secureM"
 
 
 text{*Spy has access to his own key for spoof messages, but Server is secure*}
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/TLS.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -63,13 +63,13 @@
     Session keys implicitly include MAC secrets.*)
   sessionK :: "(nat*nat*nat) * role => key"
 
-syntax
-    clientK :: "nat*nat*nat => key"
-    serverK :: "nat*nat*nat => key"
+abbreviation
+  clientK :: "nat*nat*nat => key"
+  "clientK X == sessionK(X, ClientRole)"
 
-translations
-  "clientK X" == "sessionK(X, ClientRole)"
-  "serverK X" == "sessionK(X, ServerRole)"
+  serverK :: "nat*nat*nat => key"
+  "serverK X == sessionK(X, ServerRole)"
+
 
 specification (PRF)
   inj_PRF: "inj PRF"
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -12,23 +12,18 @@
 
 theory ZhouGollmann imports Public begin
 
-syntax
+abbreviation
   TTP :: agent
+  "TTP == Server"
 
-translations
-  "TTP" == " Server "
-
-syntax
   f_sub :: nat
+  "f_sub == 5"
   f_nro :: nat
+  "f_nro == 2"
   f_nrr :: nat
+  "f_nrr == 3"
   f_con :: nat
-
-translations
-  "f_sub" == " 5 "
-  "f_nro" == " 2 "
-  "f_nrr" == " 3 "
-  "f_con" == " 4 "
+  "f_con == 4"
 
 
 constdefs
diff -r 9bc632ae588f -r 1d478c2d621f src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -110,28 +110,20 @@
                     Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
-syntax
+abbreviation
+  NP  :: xcpt
+  "NP == NullPointer"
 
-  NP  :: xcpt
   tprg  ::"java_mb prog"
+  "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
+
   obj1  :: obj
-  obj2  :: obj
-  s0  :: state
-  s1  :: state
-  s2  :: state
-  s3  :: state
-  s4  :: state
+  "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
 
-translations
-  "NP"   == "NullPointer"
-  "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
-  "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
-         ((vee, Ext )\<mapsto>Intg 0))"
-  "s0" == " Norm    (empty, empty)"
-  "s1" == " Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
-  "s2" == " Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
-  "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
-
+  "s0 == Norm    (empty, empty)"
+  "s1 == Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+  "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+  "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
 
 ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"