# HG changeset patch
# User wenzelm
# Date 1273675489 -7200
# Node ID 426d5781bb250abf895cd579d2d1f629719e01b4
# Parent  7330e4eefbd789d6803597aa88ac6ac959e5da56
modernized specifications;

diff -r 7330e4eefbd7 -r 426d5781bb25 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/FOL/FOL.thy	Wed May 12 16:44:49 2010 +0200
@@ -348,11 +348,10 @@
 
 text {* Proper handling of non-atomic rule statements. *}
 
-constdefs
-  induct_forall where "induct_forall(P) == \<forall>x. P(x)"
-  induct_implies where "induct_implies(A, B) == A \<longrightarrow> B"
-  induct_equal where "induct_equal(x, y) == x = y"
-  induct_conj where "induct_conj(A, B) == A \<and> B"
+definition "induct_forall(P) == \<forall>x. P(x)"
+definition "induct_implies(A, B) == A \<longrightarrow> B"
+definition "induct_equal(x, y) == x = y"
+definition "induct_conj(A, B) == A \<and> B"
 
 lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
   unfolding atomize_all induct_forall_def .
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Wed May 12 16:44:49 2010 +0200
@@ -21,30 +21,32 @@
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
-constdefs
+definition
  (* authKeys are those contained in an authTicket *)
-    authKeys :: "event list => key set"
-    "authKeys evs == {authK. \<exists>A Peer Ta. Says Kas A
+    authKeys :: "event list => key set" where
+    "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A
                         (Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
                (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
                   \<rbrace>) \<in> set evs}"
 
+definition
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] => bool"
-             ("_ Issues _ with _ on _")
-   "A Issues B with X on evs ==
-      \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
-      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
+             ("_ Issues _ with _ on _") where
+   "A Issues B with X on evs =
+      (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
 
+definition
  (* Yields the subtrace of a given trace from its beginning to a given event *)
   before :: "[event, event list] => event list" ("before _ on _")
-   "before ev on evs ==  takeWhile (% z. z ~= ev) (rev evs)"
+  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
 
+definition
  (* States than an event really appears only once on a trace *)
   Unique :: "[event, event list] => bool" ("Unique _ on _")
-   "Unique ev on evs == 
-      ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
 
 
 consts
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/KerberosIV_Gets.thy
--- a/src/HOL/Auth/KerberosIV_Gets.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/KerberosIV_Gets.thy	Wed May 12 16:44:49 2010 +0200
@@ -21,18 +21,18 @@
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
-constdefs
+definition
  (* authKeys are those contained in an authTicket *)
-    authKeys :: "event list => key set"
-    "authKeys evs == {authK. \<exists>A Peer Ta. Says Kas A
+    authKeys :: "event list => key set" where
+    "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A
                         (Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
                (Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
                   \<rbrace>) \<in> set evs}"
 
+definition
  (* States than an event really appears only once on a trace *)
   Unique :: "[event, event list] => bool" ("Unique _ on _")
-   "Unique ev on evs == 
-      ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
 
 
 consts
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/KerberosV.thy
--- a/src/HOL/Auth/KerberosV.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/KerberosV.thy	Wed May 12 16:44:49 2010 +0200
@@ -21,21 +21,22 @@
   Tgs_not_bad [iff]: "Tgs \<notin> bad"
    --{*Tgs is secure --- we already know that Kas is secure*}
 
-constdefs
+definition
  (* authKeys are those contained in an authTicket *)
-    authKeys :: "event list => key set"
-    "authKeys evs == {authK. \<exists>A Peer Ta. 
+    authKeys :: "event list => key set" where
+    "authKeys evs = {authK. \<exists>A Peer Ta. 
         Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Ta\<rbrace>,
                      Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Ta\<rbrace>
                    \<rbrace> \<in> set evs}"
 
+definition
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] => bool"
-             ("_ Issues _ with _ on _")
-   "A Issues B with X on evs ==
-      \<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
-      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
+             ("_ Issues _ with _ on _") where
+   "A Issues B with X on evs =
+      (\<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
+        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
 
 
 consts
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Wed May 12 16:44:49 2010 +0200
@@ -51,24 +51,24 @@
   "expiredA T evs == authlife + T < CT evs"
 
 
-constdefs
-
+definition
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] => bool"
-             ("_ Issues _ with _ on _")
-   "A Issues B with X on evs ==
-      \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
-      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
+             ("_ Issues _ with _ on _") where
+   "A Issues B with X on evs =
+      (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
 
+definition
  (* Yields the subtrace of a given trace from its beginning to a given event *)
   before :: "[event, event list] => event list" ("before _ on _")
-   "before ev on evs ==  takeWhile (% z. z ~= ev) (rev evs)"
+  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
 
+definition
  (* States than an event really appears only once on a trace *)
   Unique :: "[event, event list] => bool" ("Unique _ on _")
-   "Unique ev on evs == 
-      ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
 
 
 inductive_set bankerberos :: "event list set"
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/Kerberos_BAN_Gets.thy
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Wed May 12 16:44:49 2010 +0200
@@ -52,15 +52,15 @@
   "expiredA T evs == authlife + T < CT evs"
 
 
-constdefs
+definition
  (* Yields the subtrace of a given trace from its beginning to a given event *)
   before :: "[event, event list] => event list" ("before _ on _")
-   "before ev on evs ==  takeWhile (% z. z ~= ev) (rev evs)"
+  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
 
+definition
  (* States than an event really appears only once on a trace *)
   Unique :: "[event, event list] => bool" ("Unique _ on _")
-   "Unique ev on evs == 
-      ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
 
 
 inductive_set bankerb_gets :: "event list set"
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Wed May 12 16:44:49 2010 +0200
@@ -14,15 +14,14 @@
   Proc. Royal Soc. 426
 *}
 
-constdefs
-
+definition
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] => bool"
-             ("_ Issues _ with _ on _")
-   "A Issues B with X on evs ==
-      \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
-      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
+             ("_ Issues _ with _ on _") where
+   "A Issues B with X on evs =
+      (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
 
 
 inductive_set ns_shared :: "event list set"
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Wed May 12 16:44:49 2010 +0200
@@ -11,16 +11,22 @@
 
 section {* Machinery for the Schorr-Waite proof*}
 
-constdefs
+definition
   -- "Relations induced by a mapping"
   rel :: "('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
-  "rel m == {(x,y). m x = Ref y}"
+  where "rel m = {(x,y). m x = Ref y}"
+
+definition
   relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
-  "relS M == (\<Union> m \<in> M. rel m)"
+  where "relS M = (\<Union> m \<in> M. rel m)"
+
+definition
   addrs :: "'a ref set \<Rightarrow> 'a set"
-  "addrs P == {a. Ref a \<in> P}"
+  where "addrs P = {a. Ref a \<in> P}"
+
+definition
   reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> 'a set"
-  "reachable r P == (r\<^sup>* `` addrs P)"
+  where "reachable r P = (r\<^sup>* `` addrs P)"
 
 lemmas rel_defs = relS_def rel_def
 
@@ -77,10 +83,10 @@
 apply (simp add:rel_defs fun_upd_apply)
 done
 
-constdefs
+definition
   -- "Restriction of a relation"
   restr ::"('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set"       ("(_/ | _)" [50, 51] 50)
-  "restr r m == {(x,y). (x,y) \<in> r \<and> \<not> m x}"
+  where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> m x}"
 
 text {* Rewrite rules for the restriction of a relation *}
 
@@ -109,10 +115,10 @@
 apply (simp add:restr_def fun_upd_apply)
 done
 
-constdefs
+definition
   -- "A short form for the stack mapping function for List"
   S :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
-  "S c l r == (\<lambda>x. if c x then r x else l x)"
+  where "S c l r = (\<lambda>x. if c x then r x else l x)"
 
 text {* Rewrite rules for Lists using S as their mapping *}
 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed May 12 16:44:49 2010 +0200
@@ -93,10 +93,10 @@
 by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) 
 
 
-constdefs
+definition
   (*Keys useful to decrypt elements of a message set*)
   keysFor :: "msg set => key set"
-  "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
+  where "keysFor H = invKey ` {K. \<exists>X. Crypt K X \<in> H}"
 
 subsubsection{*Inductive definition of all "parts" of a message.*}
 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/SET_Protocol/Public_SET.thy
--- a/src/HOL/SET_Protocol/Public_SET.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Wed May 12 16:44:49 2010 +0200
@@ -119,20 +119,22 @@
 
 subsection{*Signature Primitives*}
 
-constdefs 
-
+definition
  (* Signature = Message + signed Digest *)
   sign :: "[key, msg]=>msg"
-    "sign K X == {|X, Crypt K (Hash X) |}"
+  where "sign K X = {|X, Crypt K (Hash X) |}"
 
+definition
  (* Signature Only = signed Digest Only *)
   signOnly :: "[key, msg]=>msg"
-    "signOnly K X == Crypt K (Hash X)"
+  where "signOnly K X = Crypt K (Hash X)"
 
+definition
  (* Signature for Certificates = Message + signed Message *)
   signCert :: "[key, msg]=>msg"
-    "signCert K X == {|X, Crypt K X |}"
+  where "signCert K X = {|X, Crypt K X |}"
 
+definition
  (* Certification Authority's Certificate.
     Contains agent name, a key, a number specifying the key's target use,
               a key to sign the entire certificate.
@@ -141,16 +143,16 @@
                   then Ka=pubEK i or pubSK i depending on T  ??
  *)
   cert :: "[agent, key, msg, key] => msg"
-    "cert A Ka T signK == signCert signK {|Agent A, Key Ka, T|}"
+  where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}"
 
-
+definition
  (* Cardholder's Certificate.
     Contains a PAN, the certified key Ka, the PANSecret PS,
     a number specifying the target use for Ka, the signing key signK.
  *)
   certC :: "[nat, key, nat, msg, key] => msg"
-    "certC PAN Ka PS T signK ==
-     signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
+  where "certC PAN Ka PS T signK =
+    signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
 
 (*cert and certA have no repeated elements, so they could be abbreviations,
   but that's tricky and makes proofs slower*)
@@ -164,13 +166,13 @@
 definition EXcrypt :: "[key,key,msg,msg] => msg" where
   --{*Extra Encryption*}
     (*K: the symmetric key   EK: the public encryption key*)
-    "EXcrypt K EK M m ==
+    "EXcrypt K EK M m =
        {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"
 
 definition EXHcrypt :: "[key,key,msg,msg] => msg" where
   --{*Extra Encryption with Hashing*}
     (*K: the symmetric key   EK: the public encryption key*)
-    "EXHcrypt K EK M m ==
+    "EXHcrypt K EK M m =
        {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"
 
 definition Enc :: "[key,key,key,msg] => msg" where
@@ -178,12 +180,12 @@
     (*SK: the sender's signing key
       K: the symmetric key
       EK: the public encryption key*)
-    "Enc SK K EK M ==
+    "Enc SK K EK M =
        {|Crypt K (sign SK M), Crypt EK (Key K)|}"
 
 definition EncB :: "[key,key,key,msg,msg] => msg" where
   --{*Encapsulation with Baggage.  Keys as above, and baggage b.*}
-    "EncB SK K EK M b == 
+    "EncB SK K EK M b =
        {|Enc SK K EK {|M, Hash b|}, b|}"
 
 
@@ -390,14 +392,14 @@
 
 text{*A set is expanded only if a relation is applied to it*}
 lemma def_abbrev_simp_relation:
-     "A == B ==> (A \<in> X) = (B \<in> X) &  
+     "A = B ==> (A \<in> X) = (B \<in> X) &  
                  (u = A) = (u = B) &  
                  (A = u) = (B = u)"
 by auto
 
 text{*A set is expanded only if one of the given functions is applied to it*}
 lemma def_abbrev_simp_function:
-     "A == B  
+     "A = B  
       ==> parts (insert A X) = parts (insert B X) &  
           analz (insert A X) = analz (insert B X) &  
           keysFor (insert A X) = keysFor (insert B X)"
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Wed May 12 16:44:49 2010 +0200
@@ -17,52 +17,57 @@
   mClkRcvChType = "rpcSndChType"
   mClkStType    = "(PrIds => mClkState) stfun"
 
-constdefs
+definition
   (* state predicates *)
   MClkInit      :: "mClkRcvChType => mClkStType => PrIds => stpred"
-     "MClkInit rcv cst p == PRED (cst!p = #clkA  &  ~Calling rcv p)"
+  where "MClkInit rcv cst p = PRED (cst!p = #clkA  &  ~Calling rcv p)"
 
+definition
   (* actions *)
   MClkFwd       :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
-     "MClkFwd send rcv cst p == ACT
+  where "MClkFwd send rcv cst p = ACT
                            $Calling send p
                          & $(cst!p) = #clkA
                          & Call rcv p MClkRelayArg<arg<send!p>>
                          & (cst!p)$ = #clkB
                          & unchanged (rtrner send!p)"
 
+definition
   MClkRetry     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
-     "MClkRetry send rcv cst p == ACT
+  where "MClkRetry send rcv cst p = ACT
                            $(cst!p) = #clkB
                          & res<$(rcv!p)> = #RPCFailure
                          & Call rcv p MClkRelayArg<arg<send!p>>
                          & unchanged (cst!p, rtrner send!p)"
 
+definition
   MClkReply     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
-     "MClkReply send rcv cst p == ACT
+  where "MClkReply send rcv cst p = ACT
                            ~$Calling rcv p
                          & $(cst!p) = #clkB
                          & Return send p MClkReplyVal<res<rcv!p>>
                          & (cst!p)$ = #clkA
                          & unchanged (caller rcv!p)"
 
+definition
   MClkNext      :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
-      "MClkNext send rcv cst p == ACT
+  where "MClkNext send rcv cst p = ACT
                         (  MClkFwd send rcv cst p
                          | MClkRetry send rcv cst p
                          | MClkReply send rcv cst p)"
 
-
+definition
   (* temporal *)
   MClkIPSpec    :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
-      "MClkIPSpec send rcv cst p == TEMP
+  where "MClkIPSpec send rcv cst p = TEMP
                            Init MClkInit rcv cst p
                          & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
                          & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
                          & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
 
+definition
   MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
-      "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
+  where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)"
 
 lemmas MC_action_defs =
   MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/TLA/Memory/MemClerkParameters.thy
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed May 12 16:44:49 2010 +0200
@@ -19,12 +19,14 @@
   mClkSndArgType   = "memOp"
   mClkRcvArgType   = "rpcOp"
 
-constdefs
+definition
   (* translate a memory call to an RPC call *)
   MClkRelayArg     :: "memOp => rpcOp"
-    "MClkRelayArg marg == memcall marg"
+  where "MClkRelayArg marg = memcall marg"
+
+definition
   (* translate RPC failures to memory failures *)
   MClkReplyVal     :: "Vals => Vals"
-    "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
+  where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
 
 end
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed May 12 16:44:49 2010 +0200
@@ -34,82 +34,104 @@
   cst           :: "mClkStType"
   ires          :: "resType"
 
-constdefs
+definition
   (* auxiliary predicates *)
   MVOKBARF      :: "Vals => bool"
-     "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
+  where "MVOKBARF v <-> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
+
+definition
   MVOKBA        :: "Vals => bool"
-     "MVOKBA v   == (v : MemVal) | (v = OK) | (v = BadArg)"
+  where "MVOKBA v <-> (v : MemVal) | (v = OK) | (v = BadArg)"
+
+definition
   MVNROKBA      :: "Vals => bool"
-     "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
+  where "MVNROKBA v <-> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
 
+definition
   (* tuples of state functions changed by the various components *)
   e             :: "PrIds => (bit * memOp) stfun"
-     "e p == PRED (caller memCh!p)"
+  where "e p = PRED (caller memCh!p)"
+
+definition
   c             :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
-     "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
+  where "c p = PRED (cst!p, rtrner memCh!p, caller crCh!p)"
+
+definition
   r             :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
-     "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
+  where "r p = PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
+
+definition
   m             :: "PrIds => ((bit * Vals) * Vals) stfun"
-     "m p == PRED (rtrner rmCh!p, ires!p)"
+  where "m p = PRED (rtrner rmCh!p, ires!p)"
 
+definition
   (* the environment action *)
   ENext         :: "PrIds => action"
-     "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
+  where "ENext p = ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
 
 
+definition
   (* specification of the history variable *)
   HInit         :: "histType => PrIds => stpred"
-     "HInit rmhist p == PRED rmhist!p = #histA"
+  where "HInit rmhist p = PRED rmhist!p = #histA"
 
+definition
   HNext         :: "histType => PrIds => action"
-     "HNext rmhist p == ACT (rmhist!p)$ =
+  where "HNext rmhist p = ACT (rmhist!p)$ =
                      (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
                       then #histB
                       else if (MClkReply memCh crCh cst p)
                            then #histA
                            else $(rmhist!p))"
 
+definition
   HistP         :: "histType => PrIds => temporal"
-     "HistP rmhist p == TEMP Init HInit rmhist p
-                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"
+  where "HistP rmhist p = (TEMP Init HInit rmhist p
+                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p))"
 
+definition
   Hist          :: "histType => temporal"
-      "Hist rmhist == TEMP (ALL p. HistP rmhist p)"
+  where "Hist rmhist = TEMP (ALL p. HistP rmhist p)"
 
+definition
   (* the implementation *)
   IPImp          :: "PrIds => temporal"
-     "IPImp p == TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
+  where "IPImp p = (TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
                        & MClkIPSpec memCh crCh cst p
                        & RPCIPSpec crCh rmCh rst p
                        & RPSpec rmCh mm ires p
-                       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))"
+                       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
 
+definition
   ImpInit        :: "PrIds => stpred"
-      "ImpInit p == PRED (  ~Calling memCh p
+  where "ImpInit p = PRED (  ~Calling memCh p
                           & MClkInit crCh cst p
                           & RPCInit rmCh rst p
                           & PInit ires p)"
 
+definition
   ImpNext        :: "PrIds => action"
-      "ImpNext p == ACT  [ENext p]_(e p)
+  where "ImpNext p = (ACT  [ENext p]_(e p)
                        & [MClkNext memCh crCh cst p]_(c p)
                        & [RPCNext crCh rmCh rst p]_(r p)
-                       & [RNext rmCh mm ires p]_(m p)"
+                       & [RNext rmCh mm ires p]_(m p))"
 
+definition
   ImpLive        :: "PrIds => temporal"
-      "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
+  where "ImpLive p = (TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
                         & SF(MClkReply memCh crCh cst p)_(c p)
                         & WF(RPCNext crCh rmCh rst p)_(r p)
                         & WF(RNext rmCh mm ires p)_(m p)
-                        & WF(MemReturn rmCh ires p)_(m p)"
+                        & WF(MemReturn rmCh ires p)_(m p))"
 
+definition
   Implementation :: "temporal"
-      "Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
+  where "Implementation = (TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
                                & MClkISpec memCh crCh cst
                                & RPCISpec crCh rmCh rst
-                               & IRSpec rmCh mm ires)"
+                               & IRSpec rmCh mm ires))"
 
+definition
   (* the predicate S describes the states of the implementation.
      slight simplification: two "histState" parameters instead of a
      (one- or two-element) set.
@@ -117,7 +139,7 @@
      the type definitions. The last conjunct is asserted separately as the memory
      invariant MemInv, proved in Memory.thy. *)
   S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
-      "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
+  where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED
                 Calling memCh p = #ecalling
               & Calling crCh p  = #ccalling
               & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
@@ -129,29 +151,42 @@
               & cst!p = #cs
               & rst!p = #rs
               & (rmhist!p = #hs1 | rmhist!p = #hs2)
-              & MVNROKBA<ires!p>"
+              & MVNROKBA<ires!p>)"
 
+definition
   (* predicates S1 -- S6 define special instances of S *)
   S1            :: "histType => PrIds => stpred"
-      "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
+  where "S1 rmhist p = S rmhist False False False clkA rpcA histA histA p"
+
+definition
   S2            :: "histType => PrIds => stpred"
-      "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
+  where "S2 rmhist p = S rmhist True False False clkA rpcA histA histA p"
+
+definition
   S3            :: "histType => PrIds => stpred"
-      "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
+  where "S3 rmhist p = S rmhist True True False clkB rpcA histA histB p"
+
+definition
   S4            :: "histType => PrIds => stpred"
-      "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
+  where "S4 rmhist p = S rmhist True True True clkB rpcB histA histB p"
+
+definition
   S5            :: "histType => PrIds => stpred"
-      "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
+  where "S5 rmhist p = S rmhist True True False clkB rpcB histB histB p"
+
+definition
   S6            :: "histType => PrIds => stpred"
-      "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"
+  where "S6 rmhist p = S rmhist True False False clkB rpcA histB histB p"
 
+definition
   (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
   ImpInv         :: "histType => PrIds => stpred"
-      "ImpInv rmhist p == PRED (  S1 rmhist p | S2 rmhist p | S3 rmhist p
-                                | S4 rmhist p | S5 rmhist p | S6 rmhist p)"
+  where "ImpInv rmhist p = (PRED (S1 rmhist p | S2 rmhist p | S3 rmhist p
+                                | S4 rmhist p | S5 rmhist p | S6 rmhist p))"
 
+definition
   resbar        :: "histType => resType"        (* refinement mapping *)
-      "resbar rmhist s p ==
+  where"resbar rmhist s p =
                   (if (S1 rmhist p s | S2 rmhist p s)
                    then ires s p
                    else if S3 rmhist p s
@@ -167,7 +202,7 @@
                         then MemFailure else res (crCh s p)
                    else NotAResult)" (* dummy value *)
 
-axioms
+axiomatization where
   (* the "base" variables: everything except resbar and hist (for any index) *)
   MI_base:       "basevars (caller memCh!p,
                            (rtrner memCh!p, caller crCh!p, cst!p),
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed May 12 16:44:49 2010 +0200
@@ -20,15 +20,16 @@
   clientState +
   dummy :: 'a       --{*dummy field for new variables*}
 
-constdefs
+definition
   --{*DUPLICATED FROM Client.thy, but with "tok" removed*}
   --{*Maybe want a special theory section to declare such maps*}
   non_dummy :: "'a clientState_d => clientState"
-    "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
+  where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s|)"
 
+definition
   --{*Renaming map to put a Client into the standard form*}
   client_map :: "'a clientState_d => clientState*'a"
-    "client_map == funPair non_dummy dummy"
+  where "client_map = funPair non_dummy dummy"
 
 
 record allocState =
@@ -46,78 +47,86 @@
   dummy  :: 'a                    --{*dummy field for new variables*}
 
 
-constdefs
-
 --{** Resource allocation system specification **}
 
+definition
   --{*spec (1)*}
   system_safety :: "'a systemState program set"
-    "system_safety ==
+  where "system_safety =
      Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
      \<le> NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
 
+definition
   --{*spec (2)*}
   system_progress :: "'a systemState program set"
-    "system_progress == INT i : lessThan Nclients.
+  where "system_progress = (INT i : lessThan Nclients.
                         INT h.
                           {s. h \<le> (ask o sub i o client)s} LeadsTo
-                          {s. h pfixLe (giv o sub i o client) s}"
+                          {s. h pfixLe (giv o sub i o client) s})"
 
+definition
   system_spec :: "'a systemState program set"
-    "system_spec == system_safety Int system_progress"
+  where "system_spec = system_safety Int system_progress"
 
 --{** Client specification (required) ***}
 
+definition
   --{*spec (3)*}
   client_increasing :: "'a clientState_d program set"
-    "client_increasing ==
-         UNIV guarantees  Increasing ask Int Increasing rel"
+  where "client_increasing = UNIV guarantees  Increasing ask Int Increasing rel"
 
+definition
   --{*spec (4)*}
   client_bounded :: "'a clientState_d program set"
-    "client_bounded ==
-         UNIV guarantees  Always {s. ALL elt : set (ask s). elt \<le> NbT}"
+  where "client_bounded = UNIV guarantees  Always {s. ALL elt : set (ask s). elt \<le> NbT}"
 
+definition
   --{*spec (5)*}
   client_progress :: "'a clientState_d program set"
-    "client_progress ==
+  where "client_progress =
          Increasing giv  guarantees
          (INT h. {s. h \<le> giv s & h pfixGe ask s}
                  LeadsTo {s. tokens h \<le> (tokens o rel) s})"
 
+definition
   --{*spec: preserves part*}
   client_preserves :: "'a clientState_d program set"
-    "client_preserves == preserves giv Int preserves clientState_d.dummy"
+  where "client_preserves = preserves giv Int preserves clientState_d.dummy"
 
+definition
   --{*environmental constraints*}
   client_allowed_acts :: "'a clientState_d program set"
-    "client_allowed_acts ==
+  where "client_allowed_acts =
        {F. AllowedActs F =
             insert Id (UNION (preserves (funPair rel ask)) Acts)}"
 
+definition
   client_spec :: "'a clientState_d program set"
-    "client_spec == client_increasing Int client_bounded Int client_progress
+  where "client_spec = client_increasing Int client_bounded Int client_progress
                     Int client_allowed_acts Int client_preserves"
 
 --{** Allocator specification (required) **}
 
+definition
   --{*spec (6)*}
   alloc_increasing :: "'a allocState_d program set"
-    "alloc_increasing ==
+  where "alloc_increasing =
          UNIV  guarantees
          (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
 
+definition
   --{*spec (7)*}
   alloc_safety :: "'a allocState_d program set"
-    "alloc_safety ==
+  where "alloc_safety =
          (INT i : lessThan Nclients. Increasing (sub i o allocRel))
          guarantees
          Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
          \<le> NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
 
+definition
   --{*spec (8)*}
   alloc_progress :: "'a allocState_d program set"
-    "alloc_progress ==
+  where "alloc_progress =
          (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
                                      Increasing (sub i o allocRel))
          Int
@@ -141,96 +150,104 @@
     thus h should have been a function variable.  However, only h i is ever
     looked at.*)
 
+definition
   --{*spec: preserves part*}
   alloc_preserves :: "'a allocState_d program set"
-    "alloc_preserves == preserves allocRel Int preserves allocAsk Int
+  where "alloc_preserves = preserves allocRel Int preserves allocAsk Int
                         preserves allocState_d.dummy"
 
+definition
   --{*environmental constraints*}
   alloc_allowed_acts :: "'a allocState_d program set"
-    "alloc_allowed_acts ==
+  where "alloc_allowed_acts =
        {F. AllowedActs F =
             insert Id (UNION (preserves allocGiv) Acts)}"
 
+definition
   alloc_spec :: "'a allocState_d program set"
-    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
+  where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"
 
 --{** Network specification **}
 
+definition
   --{*spec (9.1)*}
   network_ask :: "'a systemState program set"
-    "network_ask == INT i : lessThan Nclients.
+  where "network_ask = (INT i : lessThan Nclients.
                         Increasing (ask o sub i o client)  guarantees
-                        ((sub i o allocAsk) Fols (ask o sub i o client))"
+                        ((sub i o allocAsk) Fols (ask o sub i o client)))"
 
+definition
   --{*spec (9.2)*}
   network_giv :: "'a systemState program set"
-    "network_giv == INT i : lessThan Nclients.
+  where "network_giv = (INT i : lessThan Nclients.
                         Increasing (sub i o allocGiv)
                         guarantees
-                        ((giv o sub i o client) Fols (sub i o allocGiv))"
+                        ((giv o sub i o client) Fols (sub i o allocGiv)))"
 
+definition
   --{*spec (9.3)*}
   network_rel :: "'a systemState program set"
-    "network_rel == INT i : lessThan Nclients.
+  where "network_rel = (INT i : lessThan Nclients.
                         Increasing (rel o sub i o client)
                         guarantees
-                        ((sub i o allocRel) Fols (rel o sub i o client))"
+                        ((sub i o allocRel) Fols (rel o sub i o client)))"
 
+definition
   --{*spec: preserves part*}
   network_preserves :: "'a systemState program set"
-    "network_preserves ==
+  where "network_preserves =
        preserves allocGiv  Int
        (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
                                    preserves (ask o sub i o client))"
 
+definition
   --{*environmental constraints*}
   network_allowed_acts :: "'a systemState program set"
-    "network_allowed_acts ==
+  where "network_allowed_acts =
        {F. AllowedActs F =
            insert Id
             (UNION (preserves allocRel Int
                     (INT i: lessThan Nclients. preserves(giv o sub i o client)))
                   Acts)}"
 
+definition
   network_spec :: "'a systemState program set"
-    "network_spec == network_ask Int network_giv Int
+  where "network_spec = network_ask Int network_giv Int
                      network_rel Int network_allowed_acts Int
                      network_preserves"
 
 
 --{** State mappings **}
+definition
   sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
-    "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
+  where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s
                        in (| allocGiv = allocGiv s,
                              allocAsk = allocAsk s,
                              allocRel = allocRel s,
                              client   = cl,
-                             dummy    = xtr|)"
+                             dummy    = xtr|))"
 
 
+definition
   sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
-    "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
+  where "sysOfClient = (%(cl,al). (| allocGiv = allocGiv al,
                                  allocAsk = allocAsk al,
                                  allocRel = allocRel al,
                                  client   = cl,
-                                 systemState.dummy = allocState_d.dummy al|)"
+                                 systemState.dummy = allocState_d.dummy al|))"
 
-consts
-    Alloc   :: "'a allocState_d program"
-    Client  :: "'a clientState_d program"
-    Network :: "'a systemState program"
-    System  :: "'a systemState program"
+axiomatization Alloc :: "'a allocState_d program"
+  where Alloc: "Alloc : alloc_spec"
 
-axioms
-    Alloc:   "Alloc   : alloc_spec"
-    Client:  "Client  : client_spec"
-    Network: "Network : network_spec"
+axiomatization Client :: "'a clientState_d program"
+  where Client: "Client : client_spec"
 
-defs
-    System_def:
-      "System == rename sysOfAlloc Alloc Join Network Join
+axiomatization Network :: "'a systemState program"
+  where Network: "Network : network_spec"
+
+definition System  :: "'a systemState program"
+  where "System = rename sysOfAlloc Alloc Join Network Join
                  (rename sysOfClient
                   (plam x: lessThan Nclients. rename client_map Client))"
 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Wed May 12 16:44:49 2010 +0200
@@ -21,7 +21,7 @@
   dummy :: 'a       (*dummy field for new variables*)
 
 definition non_dummy :: "('a,'b) merge_d => 'b merge" where
-    "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
+    "non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)"
 
 record 'b distr =
   In  :: "'b list"          (*items to distribute*)
@@ -49,30 +49,32 @@
   dummy    :: 'a                  (*dummy field for new variables*)
 
 
-constdefs
-
 (** Merge specification (the number of inputs is Nclients) ***)
 
+definition
   (*spec (10)*)
   merge_increasing :: "('a,'b) merge_d program set"
-    "merge_increasing ==
+  where "merge_increasing =
          UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
 
+definition
   (*spec (11)*)
   merge_eqOut :: "('a,'b) merge_d program set"
-    "merge_eqOut ==
+  where "merge_eqOut =
          UNIV guarantees
          Always {s. length (merge.Out s) = length (merge.iOut s)}"
 
+definition
   (*spec (12)*)
   merge_bounded :: "('a,'b) merge_d program set"
-    "merge_bounded ==
+  where "merge_bounded =
          UNIV guarantees
          Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
 
+definition
   (*spec (13)*)
   merge_follows :: "('a,'b) merge_d program set"
-    "merge_follows ==
+  where "merge_follows =
          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
          guarantees
          (\<Inter>i \<in> lessThan Nclients.
@@ -80,25 +82,29 @@
                        {k. k < size(merge.iOut s) & merge.iOut s! k = i})
           Fols (sub i o merge.In))"
 
+definition
   (*spec: preserves part*)
   merge_preserves :: "('a,'b) merge_d program set"
-    "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
+  where "merge_preserves = preserves merge.In Int preserves merge_d.dummy"
 
+definition
   (*environmental constraints*)
   merge_allowed_acts :: "('a,'b) merge_d program set"
-    "merge_allowed_acts ==
+  where "merge_allowed_acts =
        {F. AllowedActs F =
             insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
 
+definition
   merge_spec :: "('a,'b) merge_d program set"
-    "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
+  where "merge_spec = merge_increasing Int merge_eqOut Int merge_bounded Int
                    merge_follows Int merge_allowed_acts Int merge_preserves"
 
 (** Distributor specification (the number of outputs is Nclients) ***)
 
+definition
   (*spec (14)*)
   distr_follows :: "('a,'b) distr_d program set"
-    "distr_follows ==
+  where "distr_follows =
          Increasing distr.In Int Increasing distr.iIn Int
          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
          guarantees
@@ -107,28 +113,33 @@
           (%s. sublist (distr.In s)
                        {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
 
+definition
   distr_allowed_acts :: "('a,'b) distr_d program set"
-    "distr_allowed_acts ==
+  where "distr_allowed_acts =
        {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
 
+definition
   distr_spec :: "('a,'b) distr_d program set"
-    "distr_spec == distr_follows Int distr_allowed_acts"
+  where "distr_spec = distr_follows Int distr_allowed_acts"
 
 (** Single-client allocator specification (required) ***)
 
+definition
   (*spec (18)*)
   alloc_increasing :: "'a allocState_d program set"
-    "alloc_increasing == UNIV  guarantees  Increasing giv"
+  where "alloc_increasing = UNIV  guarantees  Increasing giv"
 
+definition
   (*spec (19)*)
   alloc_safety :: "'a allocState_d program set"
-    "alloc_safety ==
+  where "alloc_safety =
          Increasing rel
          guarantees  Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}"
 
+definition
   (*spec (20)*)
   alloc_progress :: "'a allocState_d program set"
-    "alloc_progress ==
+  where "alloc_progress =
          Increasing ask Int Increasing rel Int
          Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}
          Int
@@ -137,20 +148,23 @@
                  {s. tokens h \<le> tokens (rel s)})
          guarantees  (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})"
 
+definition
   (*spec: preserves part*)
   alloc_preserves :: "'a allocState_d program set"
-    "alloc_preserves == preserves rel Int
+  where "alloc_preserves = preserves rel Int
                         preserves ask Int
                         preserves allocState_d.dummy"
 
 
+definition
   (*environmental constraints*)
   alloc_allowed_acts :: "'a allocState_d program set"
-    "alloc_allowed_acts ==
+  where "alloc_allowed_acts =
        {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
 
+definition
   alloc_spec :: "'a allocState_d program set"
-    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
+  where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"
 
 locale Merge =
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy	Wed May 12 16:44:49 2010 +0200
@@ -5,7 +5,7 @@
 
 header{*Distributed Resource Management System: the Client*}
 
-theory Client imports Rename AllocBase begin
+theory Client imports "../Rename" AllocBase begin
 
 types
   tokbag = nat     --{*tokbags could be multisets...or any ordered type?*}
@@ -23,12 +23,12 @@
 
 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
 
-constdefs
   
   (** Release some tokens **)
   
+definition
   rel_act :: "('a state_d * 'a state_d) set"
-    "rel_act == {(s,s').
+  where "rel_act = {(s,s').
                   \<exists>nrel. nrel = size (rel s) &
                          s' = s (| rel := rel s @ [giv s!nrel] |) &
                          nrel < size (giv s) &
@@ -39,15 +39,18 @@
   (** Including s'=s suppresses fairness, allowing the non-trivial part
       of the action to be ignored **)
 
+definition
   tok_act :: "('a state_d * 'a state_d) set"
-     "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
+  where "tok_act = {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
   
+definition
   ask_act :: "('a state_d * 'a state_d) set"
-    "ask_act == {(s,s'). s'=s |
+  where "ask_act = {(s,s'). s'=s |
                          (s' = s (|ask := ask s @ [tok s]|))}"
 
+definition
   Client :: "'a state_d program"
-    "Client ==
+  where "Client =
        mk_total_program
             ({s. tok s \<in> atMost NbT &
                  giv s = [] & ask s = [] & rel s = []},
@@ -55,13 +58,15 @@
              \<Union>G \<in> preserves rel Int preserves ask Int preserves tok.
                    Acts G)"
 
+definition
   (*Maybe want a special theory section to declare such maps*)
   non_dummy :: "'a state_d => state"
-    "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
+  where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
 
+definition
   (*Renaming map to put a Client into the standard form*)
   client_map :: "'a state_d => state*'a"
-    "client_map == funPair non_dummy dummy"
+  where "client_map = funPair non_dummy dummy"
 
 
 declare Client_def [THEN def_prg_Init, simp]
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Counter.thy
--- a/src/HOL/UNITY/Comp/Counter.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy	Wed May 12 16:44:49 2010 +0200
@@ -28,10 +28,10 @@
 types command = "(state*state)set"
 
 definition a :: "nat=>command" where
- "a i == {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
+ "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"
 
 definition Component :: "nat => state program" where
-  "Component i ==
+  "Component i =
     mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
                      \<Union>G \<in> preserves (%s. s (c i)). Acts G)"
 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Wed May 12 16:44:49 2010 +0200
@@ -33,12 +33,12 @@
 types command = "(state*state)set"
 
 definition a :: "nat=>command" where
- "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
+ "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
  
 definition Component :: "nat => state program" where
-  "Component i == mk_total_program({s. C s = 0 & (c s) i = 0},
-                                   {a i},
-                                   \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
+  "Component i = mk_total_program({s. C s = 0 & (c s) i = 0},
+                                  {a i},
+                                  \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
 
 
 declare Component_def [THEN def_prg_Init, simp]
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Handshake.thy
--- a/src/HOL/UNITY/Comp/Handshake.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy	Wed May 12 16:44:49 2010 +0200
@@ -15,24 +15,28 @@
   NF :: nat
   NG :: nat
 
-constdefs
+definition
   (*F's program*)
   cmdF :: "(state*state) set"
-    "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
+  where "cmdF = {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
 
+definition
   F :: "state program"
-    "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
+  where "F = mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
 
+definition
   (*G's program*)
   cmdG :: "(state*state) set"
-    "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
+  where "cmdG = {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
 
+definition
   G :: "state program"
-    "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
+  where "G = mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
 
+definition
   (*the joint invariant*)
   invFG :: "state set"
-    "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
+  where "invFG = {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
 
 
 declare F_def [THEN def_prg_Init, simp] 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/Priority.thy
--- a/src/HOL/UNITY/Comp/Priority.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy	Wed May 12 16:44:49 2010 +0200
@@ -21,51 +21,51 @@
 
 text{*Following the definitions given in section 4.4 *}
 
-definition highest :: "[vertex, (vertex*vertex)set]=>bool" where
-  "highest i r == A i r = {}"
+definition highest :: "[vertex, (vertex*vertex)set]=>bool"
+  where "highest i r <-> A i r = {}"
     --{* i has highest priority in r *}
   
-definition lowest :: "[vertex, (vertex*vertex)set]=>bool" where
-  "lowest i r == R i r = {}"
+definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
+  where "lowest i r <-> R i r = {}"
     --{* i has lowest priority in r *}
 
-definition act :: command where
-  "act i == {(s, s'). s'=reverse i s & highest i s}"
+definition act :: command
+  where "act i = {(s, s'). s'=reverse i s & highest i s}"
 
-definition Component :: "vertex=>state program" where
-  "Component i == mk_total_program({init}, {act i}, UNIV)"
+definition Component :: "vertex=>state program"
+  where "Component i = mk_total_program({init}, {act i}, UNIV)"
     --{* All components start with the same initial state *}
 
 
 text{*Some Abbreviations *}
-definition Highest :: "vertex=>state set" where
-  "Highest i == {s. highest i s}"
+definition Highest :: "vertex=>state set"
+  where "Highest i = {s. highest i s}"
 
-definition Lowest :: "vertex=>state set" where
-  "Lowest i == {s. lowest i s}"
+definition Lowest :: "vertex=>state set"
+  where "Lowest i = {s. lowest i s}"
 
-definition Acyclic :: "state set" where
-  "Acyclic == {s. acyclic s}"
+definition Acyclic :: "state set"
+  where "Acyclic = {s. acyclic s}"
 
 
-definition Maximal :: "state set" where
+definition Maximal :: "state set"
     --{* Every ``above'' set has a maximal vertex*}
-  "Maximal == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i  s. highest j s)}"
+  where "Maximal = (\<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i  s. highest j s)})"
 
-definition Maximal' :: "state set" where
+definition Maximal' :: "state set"
     --{* Maximal vertex: equivalent definition*}
-  "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)"
+  where "Maximal' = (\<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j))"
 
   
-definition Safety :: "state set" where
-  "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}"
+definition Safety :: "state set"
+  where "Safety = (\<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)})"
 
 
   (* Composition of a finite set of component;
      the vertex 'UNIV' is finite by assumption *)
   
-definition system :: "state program" where
-  "system == JN i. Component i"
+definition system :: "state program"
+  where "system = (JN i. Component i)"
 
 
 declare highest_def [simp] lowest_def [simp]
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Wed May 12 16:44:49 2010 +0200
@@ -9,14 +9,14 @@
 
 types 'a state = "nat * 'a"   (*second component allows new variables*)
 
-definition count :: "'a state => nat" where
-    "count s == fst s"
+definition count :: "'a state => nat"
+  where "count s = fst s"
   
-definition decr  :: "('a state * 'a state) set" where
-    "decr == UN n uu. {((Suc n, uu), (n,uu))}"
+definition decr  :: "('a state * 'a state) set"
+  where "decr = (UN n uu. {((Suc n, uu), (n,uu))})"
   
-definition Timer :: "'a state program" where
-    "Timer == mk_total_program (UNIV, {decr}, UNIV)"
+definition Timer :: "'a state program"
+  where "Timer = mk_total_program (UNIV, {decr}, UNIV)"
 
 
 declare Timer_def [THEN def_prg_Init, simp]
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/ELT.thy	Wed May 12 16:44:49 2010 +0200
@@ -38,20 +38,21 @@
  | Union:  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
 
 
-constdefs
-  
+definition  
   (*the set of all sets determined by f alone*)
   givenBy :: "['a => 'b] => 'a set set"
-    "givenBy f == range (%B. f-` B)"
+  where "givenBy f = range (%B. f-` B)"
 
+definition
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
                                         ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
-    "leadsETo A CC B == {F. (A,B) : elt CC F}"
+  where "leadsETo A CC B = {F. (A,B) : elt CC F}"
 
+definition
   LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
                                         ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
-    "LeadsETo A CC B ==
+  where "LeadsETo A CC B =
       {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"
 
 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Extend.thy	Wed May 12 16:44:49 2010 +0200
@@ -11,36 +11,42 @@
 
 theory Extend imports Guar begin
 
-constdefs
-
+definition
   (*MOVE to Relation.thy?*)
   Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
-    "Restrict A r == r \<inter> (A <*> UNIV)"
+  where "Restrict A r = r \<inter> (A <*> UNIV)"
 
+definition
   good_map :: "['a*'b => 'c] => bool"
-    "good_map h == surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
+  where "good_map h <-> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
      (*Using the locale constant "f", this is  f (h (x,y))) = x*)
   
+definition
   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
-    "extend_set h A == h ` (A <*> UNIV)"
+  where "extend_set h A = h ` (A <*> UNIV)"
 
+definition
   project_set :: "['a*'b => 'c, 'c set] => 'a set"
-    "project_set h C == {x. \<exists>y. h(x,y) \<in> C}"
+  where "project_set h C = {x. \<exists>y. h(x,y) \<in> C}"
 
+definition
   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
-    "extend_act h == %act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))}"
+  where "extend_act h = (%act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))})"
 
+definition
   project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
-    "project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
+  where "project_act h act = {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
 
+definition
   extend :: "['a*'b => 'c, 'a program] => 'c program"
-    "extend h F == mk_program (extend_set h (Init F),
+  where "extend h F = mk_program (extend_set h (Init F),
                                extend_act h ` Acts F,
                                project_act h -` AllowedActs F)"
 
+definition
   (*Argument C allows weak safety laws to be projected*)
   project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
-    "project h C F ==
+  where "project h C F =
        mk_program (project_set h (Init F),
                    project_act h ` Restrict C ` Acts F,
                    {act. Restrict (project_set h C) act :
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Simple/Lift.thy
--- a/src/HOL/UNITY/Simple/Lift.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy	Wed May 12 16:44:49 2010 +0200
@@ -18,98 +18,116 @@
   up    :: "bool"           --{*current direction of movement*}
   move  :: "bool"           --{*whether moving takes precedence over opening*}
 
-consts
-  Min :: "int"       --{*least and greatest floors*}
+axiomatization
+  Min :: "int" and   --{*least and greatest floors*}
   Max :: "int"       --{*least and greatest floors*}
-
-axioms
+where
   Min_le_Max [iff]: "Min \<le> Max"
   
-constdefs
   
   --{*Abbreviations: the "always" part*}
   
+definition
   above :: "state set"
-    "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
+  where "above = {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
 
+definition
   below :: "state set"
-    "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
+  where "below = {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
 
+definition
   queueing :: "state set"
-    "queueing == above \<union> below"
+  where "queueing = above \<union> below"
 
+definition
   goingup :: "state set"
-    "goingup   == above \<inter> ({s. up s}  \<union> -below)"
+  where "goingup = above \<inter> ({s. up s}  \<union> -below)"
 
+definition
   goingdown :: "state set"
-    "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
+  where "goingdown = below \<inter> ({s. ~ up s} \<union> -above)"
 
+definition
   ready :: "state set"
-    "ready == {s. stop s & ~ open s & move s}"
+  where "ready = {s. stop s & ~ open s & move s}"
  
   --{*Further abbreviations*}
 
+definition
   moving :: "state set"
-    "moving ==  {s. ~ stop s & ~ open s}"
+  where "moving = {s. ~ stop s & ~ open s}"
 
+definition
   stopped :: "state set"
-    "stopped == {s. stop s  & ~ open s & ~ move s}"
+  where "stopped = {s. stop s  & ~ open s & ~ move s}"
 
+definition
   opened :: "state set"
-    "opened ==  {s. stop s  &  open s  &  move s}"
+  where "opened = {s. stop s  &  open s  &  move s}"
 
+definition
   closed :: "state set"  --{*but this is the same as ready!!*}
-    "closed ==  {s. stop s  & ~ open s &  move s}"
+  where "closed = {s. stop s  & ~ open s &  move s}"
 
+definition
   atFloor :: "int => state set"
-    "atFloor n ==  {s. floor s = n}"
+  where "atFloor n = {s. floor s = n}"
 
+definition
   Req :: "int => state set"
-    "Req n ==  {s. n \<in> req s}"
+  where "Req n = {s. n \<in> req s}"
 
 
   
   --{*The program*}
   
+definition
   request_act :: "(state*state) set"
-    "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
+  where "request_act = {(s,s'). s' = s (|stop:=True, move:=False|)
                                   & ~ stop s & floor s \<in> req s}"
 
+definition
   open_act :: "(state*state) set"
-    "open_act ==
+  where "open_act =
          {(s,s'). s' = s (|open :=True,
                            req  := req s - {floor s},
                            move := True|)
                        & stop s & ~ open s & floor s \<in> req s
                        & ~(move s & s \<in> queueing)}"
 
+definition
   close_act :: "(state*state) set"
-    "close_act == {(s,s'). s' = s (|open := False|) & open s}"
+  where "close_act = {(s,s'). s' = s (|open := False|) & open s}"
 
+definition
   req_up :: "(state*state) set"
-    "req_up ==
+  where "req_up =
          {(s,s'). s' = s (|stop  :=False,
                            floor := floor s + 1,
                            up    := True|)
                        & s \<in> (ready \<inter> goingup)}"
 
+definition
   req_down :: "(state*state) set"
-    "req_down ==
+  where "req_down =
          {(s,s'). s' = s (|stop  :=False,
                            floor := floor s - 1,
                            up    := False|)
                        & s \<in> (ready \<inter> goingdown)}"
 
+definition
   move_up :: "(state*state) set"
-    "move_up ==
+  where "move_up =
          {(s,s'). s' = s (|floor := floor s + 1|)
                        & ~ stop s & up s & floor s \<notin> req s}"
 
+definition
   move_down :: "(state*state) set"
-    "move_down ==
+  where "move_down =
          {(s,s'). s' = s (|floor := floor s - 1|)
                        & ~ stop s & ~ up s & floor s \<notin> req s}"
 
+definition
   button_press  :: "(state*state) set"
       --{*This action is omitted from prior treatments, which therefore are
         unrealistic: nobody asks the lift to do anything!  But adding this
@@ -117,14 +135,15 @@
         "ensures" properties fail. Maybe it should be constrained to only
         allow button presses in the current direction of travel, like in a
         real lift.*}
-    "button_press ==
+  where "button_press =
          {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
                         & Min \<le> n & n \<le> Max}"
 
 
+definition
   Lift :: "state program"
     --{*for the moment, we OMIT @{text button_press}*}
-    "Lift == mk_total_program
+  where "Lift = mk_total_program
                 ({s. floor s = Min & ~ up s & move s & stop s &
                           ~ open s & req s = {}},
                  {request_act, open_act, close_act,
@@ -134,34 +153,41 @@
 
   --{*Invariants*}
 
+definition
   bounded :: "state set"
-    "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
+  where "bounded = {s. Min \<le> floor s & floor s \<le> Max}"
 
+definition
   open_stop :: "state set"
-    "open_stop == {s. open s --> stop s}"
+  where "open_stop = {s. open s --> stop s}"
   
+definition
   open_move :: "state set"
-    "open_move == {s. open s --> move s}"
+  where "open_move = {s. open s --> move s}"
   
+definition
   stop_floor :: "state set"
-    "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
+  where "stop_floor = {s. stop s & ~ move s --> floor s \<in> req s}"
   
+definition
   moving_up :: "state set"
-    "moving_up == {s. ~ stop s & up s -->
+  where "moving_up = {s. ~ stop s & up s -->
                    (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
   
+definition
   moving_down :: "state set"
-    "moving_down == {s. ~ stop s & ~ up s -->
+  where "moving_down = {s. ~ stop s & ~ up s -->
                      (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
   
+definition
   metric :: "[int,state] => int"
-    "metric ==
-       %n s. if floor s < n then (if up s then n - floor s
+  where "metric =
+       (%n s. if floor s < n then (if up s then n - floor s
                                   else (floor s - Min) + (n-Min))
              else
              if n < floor s then (if up s then (Max - floor s) + (Max-n)
                                   else floor s - n)
-             else 0"
+             else 0)"
 
 locale Floor =
   fixes n
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Simple/Mutex.thy
--- a/src/HOL/UNITY/Simple/Mutex.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy	Wed May 12 16:44:49 2010 +0200
@@ -16,44 +16,43 @@
 
 types command = "(state*state) set"
 
-constdefs
-  
+
   (** The program for process U **)
   
-  U0 :: command
-    "U0 == {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}"
+definition U0 :: command
+  where "U0 = {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}"
 
-  U1 :: command
-    "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}"
+definition  U1 :: command
+  where "U1 = {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}"
 
-  U2 :: command
-    "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
+definition  U2 :: command
+  where "U2 = {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}"
 
-  U3 :: command
-    "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
+definition  U3 :: command
+  where "U3 = {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}"
 
-  U4 :: command
-    "U4 == {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}"
+definition  U4 :: command
+  where "U4 = {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}"
 
   (** The program for process V **)
   
-  V0 :: command
-    "V0 == {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}"
+definition  V0 :: command
+  where "V0 = {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}"
 
-  V1 :: command
-    "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}"
+definition  V1 :: command
+  where "V1 = {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}"
 
-  V2 :: command
-    "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
+definition  V2 :: command
+  where "V2 = {(s,s'). s' = s (|n:=3|) & p s & n s = 2}"
 
-  V3 :: command
-    "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
+definition  V3 :: command
+  where "V3 = {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}"
 
-  V4 :: command
-    "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
+definition  V4 :: command
+  where "V4 = {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
 
-  Mutex :: "state program"
-    "Mutex == mk_total_program
+definition  Mutex :: "state program"
+  where "Mutex = mk_total_program
                  ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
                   {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
                   UNIV)"
@@ -61,16 +60,16 @@
 
   (** The correct invariants **)
 
-  IU :: "state set"
-    "IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
+definition  IU :: "state set"
+  where "IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
 
-  IV :: "state set"
-    "IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
+definition  IV :: "state set"
+  where "IV = {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
 
   (** The faulty invariant (for U alone) **)
 
-  bad_IU :: "state set"
-    "bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) &
+definition  bad_IU :: "state set"
+  where "bad_IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) &
                    (3 \<le> m s & m s \<le> 4 --> ~ p s)}"
 
 
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed May 12 16:44:49 2010 +0200
@@ -17,36 +17,38 @@
 
 types state = "event list"
 
-constdefs
-
   (*The spy MAY say anything he CAN say.  We do not expect him to
     invent new nonces here, but he can also use NS1.  Common to
     all similar protocols.*)
+definition
   Fake :: "(state*state) set"
-    "Fake == {(s,s').
+  where "Fake = {(s,s').
               \<exists>B X. s' = Says Spy B X # s
                     & X \<in> synth (analz (spies s))}"
 
   (*The numeric suffixes on A identify the rule*)
 
   (*Alice initiates a protocol run, sending a nonce to Bob*)
+definition
   NS1 :: "(state*state) set"
-    "NS1 == {(s1,s').
+  where "NS1 = {(s1,s').
              \<exists>A1 B NA.
                  s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
                & Nonce NA \<notin> used s1}"
 
   (*Bob responds to Alice's message with a further nonce*)
+definition
   NS2 :: "(state*state) set"
-    "NS2 == {(s2,s').
+  where "NS2 = {(s2,s').
              \<exists>A' A2 B NA NB.
                  s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
                & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \<in> set s2
                & Nonce NB \<notin> used s2}"
 
   (*Alice proves her existence by sending NB back to Bob.*)
+definition
   NS3 :: "(state*state) set"
-    "NS3 == {(s3,s').
+  where "NS3 = {(s3,s').
              \<exists>A3 B' B NA NB.
                  s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
                & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \<in> set s3
@@ -55,7 +57,7 @@
 
 definition Nprg :: "state program" where
     (*Initial trace is empty*)
-    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
+    "Nprg = mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
 
 declare spies_partsEs [elim]
 declare analz_into_parts [dest]
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Wed May 12 16:44:49 2010 +0200
@@ -17,20 +17,20 @@
 
   edges :: "(vertex*vertex) set"
 
-definition asgt :: "[vertex,vertex] => (state*state) set" where
-    "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
+definition asgt :: "[vertex,vertex] => (state*state) set"
+  where "asgt u v = {(s,s'). s' = s(v:= s u | s v)}"
 
-definition Rprg :: "state program" where
-    "Rprg == mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
+definition Rprg :: "state program"
+  where "Rprg = mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
 
-definition reach_invariant :: "state set" where
-    "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
+definition reach_invariant :: "state set"
+  where "reach_invariant = {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
 
-definition fixedpoint :: "state set" where
-    "fixedpoint == {s. \<forall>(u,v)\<in>edges. s u --> s v}"
+definition fixedpoint :: "state set"
+  where "fixedpoint = {s. \<forall>(u,v)\<in>edges. s u --> s v}"
 
-definition metric :: "state => nat" where
-    "metric s == card {v. ~ s v}"
+definition metric :: "state => nat"
+  where "metric s = card {v. ~ s v}"
 
 
 text{**We assume that the set of vertices is finite*}
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Wed May 12 16:44:49 2010 +0200
@@ -431,26 +431,26 @@
 text{*They avoid expanding the full program, which is a large expression*}
 
 lemma def_prg_Init:
-     "F == mk_total_program (init,acts,allowed) ==> Init F = init"
+     "F = mk_total_program (init,acts,allowed) ==> Init F = init"
 by (simp add: mk_total_program_def)
 
 lemma def_prg_Acts:
-     "F == mk_total_program (init,acts,allowed) 
+     "F = mk_total_program (init,acts,allowed) 
       ==> Acts F = insert Id (totalize_act ` acts)"
 by (simp add: mk_total_program_def)
 
 lemma def_prg_AllowedActs:
-     "F == mk_total_program (init,acts,allowed)  
+     "F = mk_total_program (init,acts,allowed)  
       ==> AllowedActs F = insert Id allowed"
 by (simp add: mk_total_program_def)
 
 text{*An action is expanded if a pair of states is being tested against it*}
 lemma def_act_simp:
-     "act == {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
+     "act = {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
 by (simp add: mk_total_program_def)
 
 text{*A set is expanded only if an element is being tested against it*}
-lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
+lemma def_set_simp: "A = B ==> (x \<in> A) = (x \<in> B)"
 by (simp add: mk_total_program_def)
 
 subsubsection{*Inspectors for type "program"*}
diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/UNITY/Union.thy	Wed May 12 16:44:49 2010 +0200
@@ -9,31 +9,35 @@
 
 theory Union imports SubstAx FP begin
 
-constdefs
-
   (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
+definition
   ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
-    "F ok G == Acts F \<subseteq> AllowedActs G &
+  where "F ok G == Acts F \<subseteq> AllowedActs G &
                Acts G \<subseteq> AllowedActs F"
 
   (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
+definition
   OK  :: "['a set, 'a => 'b program] => bool"
-    "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
+  where "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
 
+definition
   JOIN  :: "['a set, 'a => 'b program] => 'b program"
-    "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
+  where "JOIN I F = mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
                              \<Inter>i \<in> I. AllowedActs (F i))"
 
+definition
   Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
-    "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
+  where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
                              AllowedActs F \<inter> AllowedActs G)"
 
+definition
   SKIP :: "'a program"
-    "SKIP == mk_program (UNIV, {}, UNIV)"
+  where "SKIP = mk_program (UNIV, {}, UNIV)"
 
   (*Characterizes safety properties.  Used with specifying Allowed*)
+definition
   safety_prop :: "'a program set => bool"
-    "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+  where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
 
 notation (xsymbols)
   SKIP  ("\<bottom>") and
@@ -420,12 +424,12 @@
 by (simp add: Allowed_def) 
 
 lemma def_total_prg_Allowed:
-     "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
+     "[| F = mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
       ==> Allowed F = X"
 by (simp add: mk_total_program_def def_prg_Allowed) 
 
 lemma def_UNION_ok_iff:
-     "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
+     "[| F = mk_program(init,acts,UNION X Acts); safety_prop X |]  
       ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
 by (auto simp add: ok_def safety_prop_Acts_iff)