--- a/src/HOL/SET_Protocol/Message_SET.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Wed Feb 10 00:46:56 2010 +0100
@@ -71,14 +71,14 @@
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "MPair x y"
+ "{|x, y|}" == "CONST MPair x y"
constdefs
--- a/src/HOL/SET_Protocol/Public_SET.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy Wed Feb 10 00:46:56 2010 +0100
@@ -23,19 +23,12 @@
publicKey :: "[bool, agent] => key"
--{*the boolean is TRUE if a signing key*}
-syntax
- pubEK :: "agent => key"
- pubSK :: "agent => key"
- priEK :: "agent => key"
- priSK :: "agent => key"
+abbreviation "pubEK == publicKey False"
+abbreviation "pubSK == publicKey True"
-translations
- "pubEK" == "publicKey False"
- "pubSK" == "publicKey True"
-
- (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
- "priEK A" == "invKey (pubEK A)"
- "priSK A" == "invKey (pubSK A)"
+(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
+abbreviation "priEK A == invKey (pubEK A)"
+abbreviation "priSK A == invKey (pubSK A)"
text{*By freeness of agents, no two agents have the same key. Since
@{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
@@ -159,18 +152,12 @@
"certC PAN Ka PS T signK ==
signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
- (*cert and certA have no repeated elements, so they could be translations,
- but that's tricky and makes proofs slower*)
+(*cert and certA have no repeated elements, so they could be abbreviations,
+ but that's tricky and makes proofs slower*)
-syntax
- "onlyEnc" :: msg
- "onlySig" :: msg
- "authCode" :: msg
-
-translations
- "onlyEnc" == "Number 0"
- "onlySig" == "Number (Suc 0)"
- "authCode" == "Number (Suc (Suc 0))"
+abbreviation "onlyEnc == Number 0"
+abbreviation "onlySig == Number (Suc 0)"
+abbreviation "authCode == Number (Suc (Suc 0))"
subsection{*Encryption Primitives*}
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Feb 10 00:46:56 2010 +0100
@@ -55,10 +55,10 @@
"_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90)
translations
- "_slice" == "slice"
+ "_slice" == "CONST slice"
- "_Call" == "ACall"
- "_Return" == "AReturn"
+ "_Call" == "CONST ACall"
+ "_Return" == "CONST AReturn"
defs
slice_def: "(PRED (x!i)) s == x s i"
--- a/src/HOL/TLA/TLA.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/TLA/TLA.thy Wed Feb 10 00:46:56 2010 +0100
@@ -37,12 +37,12 @@
"_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10)
translations
- "_Box" == "Box"
- "_Dmd" == "Dmd"
- "_leadsto" == "leadsto"
- "_stable" == "Stable"
- "_WF" == "WF"
- "_SF" == "SF"
+ "_Box" == "CONST Box"
+ "_Dmd" == "CONST Dmd"
+ "_leadsto" == "CONST leadsto"
+ "_stable" == "CONST Stable"
+ "_WF" == "CONST WF"
+ "_SF" == "CONST SF"
"_EEx v A" == "Eex v. A"
"_AAll v A" == "Aall v. A"
--- a/src/HOL/UNITY/Union.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/UNITY/Union.thy Wed Feb 10 00:46:56 2010 +0100
@@ -42,7 +42,7 @@
translations
"JN x: A. B" == "CONST JOIN A (%x. B)"
"JN x y. B" == "JN x. JN y. B"
- "JN x. B" == "JOIN CONST UNIV (%x. B)"
+ "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
syntax (xsymbols)
SKIP :: "'a program" ("\<bottom>")
--- a/src/HOL/Word/WordDefinition.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/HOL/Word/WordDefinition.thy Wed Feb 10 00:46:56 2010 +0100
@@ -94,7 +94,7 @@
syntax
of_int :: "int => 'a"
translations
- "case x of of_int y => b" == "CONST word_int_case (%y. b) x"
+ "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
subsection "Arithmetic operations"
--- a/src/ZF/IMP/Com.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/ZF/IMP/Com.thy Wed Feb 10 00:46:56 2010 +0100
@@ -22,8 +22,10 @@
consts evala :: i
-syntax "_evala" :: "[i, i] => o" (infixl "-a->" 50)
-translations "p -a-> n" == "<p,n> \<in> evala"
+
+abbreviation
+ evala_syntax :: "[i, i] => o" (infixl "-a->" 50)
+ where "p -a-> n == <p,n> \<in> evala"
inductive
domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat"
@@ -50,8 +52,10 @@
consts evalb :: i
-syntax "_evalb" :: "[i,i] => o" (infixl "-b->" 50)
-translations "p -b-> b" == "<p,b> \<in> evalb"
+
+abbreviation
+ evalb_syntax :: "[i,i] => o" (infixl "-b->" 50)
+ where "p -b-> b == <p,b> \<in> evalb"
inductive
domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool"
@@ -82,8 +86,10 @@
consts evalc :: i
-syntax "_evalc" :: "[i, i] => o" (infixl "-c->" 50)
-translations "p -c-> s" == "<p,s> \<in> evalc"
+
+abbreviation
+ evalc_syntax :: "[i, i] => o" (infixl "-c->" 50)
+ where "p -c-> s == <p,s> \<in> evalc"
inductive
domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)"
--- a/src/ZF/Induct/Comb.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/ZF/Induct/Comb.thy Wed Feb 10 00:46:56 2010 +0100
@@ -30,12 +30,14 @@
consts
contract :: i
-syntax
- "_contract" :: "[i,i] => o" (infixl "-1->" 50)
- "_contract_multi" :: "[i,i] => o" (infixl "--->" 50)
-translations
- "p -1-> q" == "<p,q> \<in> contract"
- "p ---> q" == "<p,q> \<in> contract^*"
+
+abbreviation
+ contract_syntax :: "[i,i] => o" (infixl "-1->" 50)
+ where "p -1-> q == <p,q> \<in> contract"
+
+abbreviation
+ contract_multi :: "[i,i] => o" (infixl "--->" 50)
+ where "p ---> q == <p,q> \<in> contract^*"
syntax (xsymbols)
"comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90)
@@ -56,12 +58,14 @@
consts
parcontract :: i
-syntax
- "_parcontract" :: "[i,i] => o" (infixl "=1=>" 50)
- "_parcontract_multi" :: "[i,i] => o" (infixl "===>" 50)
-translations
- "p =1=> q" == "<p,q> \<in> parcontract"
- "p ===> q" == "<p,q> \<in> parcontract^+"
+
+abbreviation
+ parcontract_syntax :: "[i,i] => o" (infixl "=1=>" 50)
+ where "p =1=> q == <p,q> \<in> parcontract"
+
+abbreviation
+ parcontract_multi :: "[i,i] => o" (infixl "===>" 50)
+ where "p ===> q == <p,q> \<in> parcontract^+"
inductive
domains "parcontract" \<subseteq> "comb \<times> comb"
--- a/src/ZF/Induct/PropLog.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/ZF/Induct/PropLog.thy Wed Feb 10 00:46:56 2010 +0100
@@ -34,8 +34,10 @@
subsection {* The proof system *}
consts thms :: "i => i"
-syntax "_thms" :: "[i,i] => o" (infixl "|-" 50)
-translations "H |- p" == "p \<in> thms(H)"
+
+abbreviation
+ thms_syntax :: "[i,i] => o" (infixl "|-" 50)
+ where "H |- p == p \<in> thms(H)"
inductive
domains "thms(H)" \<subseteq> "propn"
--- a/src/ZF/List_ZF.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/ZF/List_ZF.thy Wed Feb 10 00:46:56 2010 +0100
@@ -19,9 +19,9 @@
"@List" :: "is => i" ("[(_)]")
translations
- "[x, xs]" == "Cons(x, [xs])"
- "[x]" == "Cons(x, [])"
- "[]" == "Nil"
+ "[x, xs]" == "CONST Cons(x, [xs])"
+ "[x]" == "CONST Cons(x, [])"
+ "[]" == "CONST Nil"
consts
--- a/src/ZF/ZF.thy Wed Feb 10 00:45:16 2010 +0100
+++ b/src/ZF/ZF.thy Wed Feb 10 00:46:56 2010 +0100
@@ -127,23 +127,23 @@
"@patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
translations
- "{x, xs}" == "cons(x, {xs})"
- "{x}" == "cons(x, 0)"
- "{x:A. P}" == "Collect(A, %x. P)"
- "{y. x:A, Q}" == "Replace(A, %x y. Q)"
- "{b. x:A}" == "RepFun(A, %x. b)"
- "INT x:A. B" == "Inter({B. x:A})"
- "UN x:A. B" == "Union({B. x:A})"
- "PROD x:A. B" == "Pi(A, %x. B)"
- "SUM x:A. B" == "Sigma(A, %x. B)"
- "lam x:A. f" == "Lambda(A, %x. f)"
- "ALL x:A. P" == "Ball(A, %x. P)"
- "EX x:A. P" == "Bex(A, %x. P)"
+ "{x, xs}" == "CONST cons(x, {xs})"
+ "{x}" == "CONST cons(x, 0)"
+ "{x:A. P}" == "CONST Collect(A, %x. P)"
+ "{y. x:A, Q}" == "CONST Replace(A, %x y. Q)"
+ "{b. x:A}" == "CONST RepFun(A, %x. b)"
+ "INT x:A. B" == "CONST Inter({B. x:A})"
+ "UN x:A. B" == "CONST Union({B. x:A})"
+ "PROD x:A. B" == "CONST Pi(A, %x. B)"
+ "SUM x:A. B" == "CONST Sigma(A, %x. B)"
+ "lam x:A. f" == "CONST Lambda(A, %x. f)"
+ "ALL x:A. P" == "CONST Ball(A, %x. P)"
+ "EX x:A. P" == "CONST Bex(A, %x. P)"
"<x, y, z>" == "<x, <y, z>>"
- "<x, y>" == "Pair(x, y)"
- "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
- "%<x,y>.b" == "split(%x y. b)"
+ "<x, y>" == "CONST Pair(x, y)"
+ "%<x,y,zs>.b" == "CONST split(%x <y,zs>.b)"
+ "%<x,y>.b" == "CONST split(%x y. b)"
notation (xsymbols)