--- a/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Mon Mar 01 13:40:23 2010 +0100
@@ -43,15 +43,11 @@
shrK_disj_pin [iff]: "shrK P \<noteq> pin Q"
crdK_disj_pin [iff]: "crdK C \<noteq> pin P"
-constdefs
- legalUse :: "card => bool" ("legalUse (_)")
+definition legalUse :: "card => bool" ("legalUse (_)") where
"legalUse C == C \<notin> stolen"
-consts
- illegalUse :: "card => bool"
-primrec
- illegalUse_def:
- "illegalUse (Card A) = ( (Card A \<in> stolen \<and> A \<in> bad) \<or> Card A \<in> cloned )"
+primrec illegalUse :: "card => bool" where
+ illegalUse_def: "illegalUse (Card A) = ( (Card A \<in> stolen \<and> A \<in> bad) \<or> Card A \<in> cloned )"
text{*initState must be defined with care*}