src/HOL/Auth/Guard/P2.thy

--- a/src/HOL/Auth/Guard/P2.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Auth/Guard/P2.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -26,7 +26,7 @@
 subsubsection{*offer chaining:
 B chains his offer for A with the head offer of L for sending it to C*}
 
-constdefs chain :: "agent => nat => agent => msg => agent => msg"
+definition chain :: "agent => nat => agent => msg => agent => msg" where
 "chain B ofr A L C ==
 let m1= sign B (Nonce ofr) in
 let m2= Hash {|head L, Agent C|} in
@@ -73,7 +73,7 @@
 
 subsubsection{*anchor of the offer list*}
 
-constdefs anchor :: "agent => nat => agent => msg"
+definition anchor :: "agent => nat => agent => msg" where
 "anchor A n B == chain A n A (cons nil nil) B"
 
 lemma anchor_inj [iff]:
@@ -88,7 +88,7 @@
 
 subsubsection{*request event*}
 
-constdefs reqm :: "agent => nat => nat => msg => agent => msg"
+definition reqm :: "agent => nat => nat => msg => agent => msg" where
 "reqm A r n I B == {|Agent A, Number r, cons (Agent A) (cons (Agent B) I),
 cons (anchor A n B) nil|}"
 
@@ -99,7 +99,7 @@
 lemma Nonce_in_reqm [iff]: "Nonce n:parts {reqm A r n I B}"
 by (auto simp: reqm_def)
 
-constdefs req :: "agent => nat => nat => msg => agent => event"
+definition req :: "agent => nat => nat => msg => agent => event" where
 "req A r n I B == Says A B (reqm A r n I B)"
 
 lemma req_inj [iff]: "(req A r n I B = req A' r' n' I' B')
@@ -108,8 +108,8 @@
 
 subsubsection{*propose event*}
 
-constdefs prom :: "agent => nat => agent => nat => msg => msg =>
-msg => agent => msg"
+definition prom :: "agent => nat => agent => nat => msg => msg =>
+msg => agent => msg" where
 "prom B ofr A r I L J C == {|Agent A, Number r,
 app (J, del (Agent B, I)), cons (chain B ofr A L C) L|}"
 
@@ -120,8 +120,8 @@
 lemma Nonce_in_prom [iff]: "Nonce ofr:parts {prom B ofr A r I L J C}"
 by (auto simp: prom_def)
 
-constdefs pro :: "agent => nat => agent => nat => msg => msg =>
-                  msg => agent => event"
+definition pro :: "agent => nat => agent => nat => msg => msg =>
+                  msg => agent => event" where
 "pro B ofr A r I L J C == Says B C (prom B ofr A r I L J C)"
 
 lemma pro_inj [dest]: "pro B ofr A r I L J C = pro B' ofr' A' r' I' L' J' C'