--- a/src/HOL/Auth/Guard/GuardK.thy Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Mon Mar 01 16:42:45 2010 +0100
@@ -176,11 +176,9 @@
subsection{*number of Crypt's in a message*}
-consts crypt_nb :: "msg => nat"
-
-recdef crypt_nb "measure size"
-"crypt_nb (Crypt K X) = Suc (crypt_nb X)"
-"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
+fun crypt_nb :: "msg => nat" where
+"crypt_nb (Crypt K X) = Suc (crypt_nb X)" |
+"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" |
"crypt_nb X = 0" (* otherwise *)
subsection{*basic facts about @{term crypt_nb}*}
@@ -190,10 +188,8 @@
subsection{*number of Crypt's in a message list*}
-consts cnb :: "msg list => nat"
-
-recdef cnb "measure size"
-"cnb [] = 0"
+primrec cnb :: "msg list => nat" where
+"cnb [] = 0" |
"cnb (X#l) = crypt_nb X + cnb l"
subsection{*basic facts about @{term cnb}*}