--- a/src/HOL/Auth/Guard/GuardK.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Mon Mar 01 13:40:23 2010 +0100
@@ -85,7 +85,7 @@
subsection{*guarded sets*}
-constdefs GuardK :: "nat => key set => msg set => bool"
+definition GuardK :: "nat => key set => msg set => bool" where
"GuardK n Ks H == ALL X. X:H --> X:guardK n Ks"
subsection{*basic facts about @{term GuardK}*}
@@ -239,7 +239,7 @@
subsection{*list corresponding to "decrypt"*}
-constdefs decrypt' :: "msg list => key => msg => msg list"
+definition decrypt' :: "msg list => key => msg => msg list" where
"decrypt' l K Y == Y # remove l (Crypt K Y)"
declare decrypt'_def [simp]