src/HOL/Auth/Guard/Guard_Shared.thy

   Ciph :: "agent => msg => msg" where
   "Ciph A X == Crypt (shrK A) X"
 
 subsubsection{*agent associated to a key*}
 
-constdefs agt :: "key => agent"
+definition agt :: "key => agent" where
 "agt K == @A. K = shrK A"
 
 lemma agt_shrK [simp]: "agt (shrK A) = A"
 by (simp add: agt_def)
 

 lemma keyset_init [iff]: "keyset (initState A)"
 by (cases A, auto simp: keyset_def initState.simps)
 
 subsubsection{*sets of symmetric keys*}
 
-constdefs shrK_set :: "key set => bool"
+definition shrK_set :: "key set => bool" where
 "shrK_set Ks == ALL K. K:Ks --> (EX A. K = shrK A)"
 
 lemma in_shrK_set: "[| shrK_set Ks; K:Ks |] ==> EX A. K = shrK A"
 by (simp add: shrK_set_def)
 

 lemma shrK_set2 [iff]: "shrK_set {shrK A, shrK B}"
 by (simp add: shrK_set_def)
 
 subsubsection{*sets of good keys*}
 
-constdefs good :: "key set => bool"
+definition good :: "key set => bool" where
 "good Ks == ALL K. K:Ks --> agt K ~:bad"
 
 lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
 by (simp add: good_def)
 

 apply (rule_tac H="knows_max (Friend C) evs" in GuardK_mono)
 by (auto simp: knows_max_def)
 
 subsubsection{*regular protocols*}
 
-constdefs regular :: "event list set => bool"
+definition regular :: "event list set => bool" where
 "regular p == ALL evs A. evs:p --> (Key (shrK A):parts (spies evs)) = (A:bad)"
 
 lemma shrK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>
 (Key (shrK A):parts (spies evs)) = (A:bad)"
 by (auto simp: regular_def)