--- a/doc-src/TutorialI/Protocol/Message.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Thu Feb 11 21:33:25 2010 +0100
@@ -82,14 +82,14 @@
(*<*)
text{*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/Auth/Message.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/Auth/Message.thy Thu Feb 11 21:33:25 2010 +0100
@@ -51,10 +51,10 @@
text{*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|}|}"
--- a/src/HOL/Metis_Examples/Message.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Thu Feb 11 21:33:25 2010 +0100
@@ -45,10 +45,10 @@
text{*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|}|}"
--- a/src/HOL/MicroJava/DFA/Product.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy Thu Feb 11 21:33:25 2010 +0100
@@ -19,9 +19,10 @@
esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
-syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
+abbreviation
+ lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
-translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
+ where "p <=(rA,rB) q == p <=_(le rA rB) q"
lemma unfold_lesub_prod:
"p <=(rA,rB) q == le rA rB p q"
--- a/src/HOL/MicroJava/DFA/Semilat.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Thu Feb 11 21:33:25 2010 +0100
@@ -33,9 +33,9 @@
"plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(*<*)
(* allow \<sub> instead of \<bsub>..\<esub> *)
- "@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
- "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
- "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+ "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
+ "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
+ "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
translations
"x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Thu Feb 11 21:33:25 2010 +0100
@@ -15,7 +15,7 @@
"x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
consts
- "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+ plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
primrec
"[] ++_f y = y"
"(x#xs) ++_f y = xs ++_f (x +_f y)"
--- a/src/HOL/Modelcheck/MuckeSyn.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Thu Feb 11 21:33:25 2010 +0100
@@ -38,7 +38,7 @@
"_idts" :: "[idt, idts] => idts" ("_,/ _" [1, 0] 0)
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)")
-(* "@pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0)
+(* "_pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0)
"_pattern" :: "[pttrn, patterns] => pttrn" ("_,/ _" [1, 0] 0) *)
"_decl" :: "[mutype,pttrn] => decl" ("_ _")
--- a/src/HOL/Prolog/Test.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/Prolog/Test.thy Thu Feb 11 21:33:25 2010 +0100
@@ -18,7 +18,7 @@
syntax
(* list Enumeration *)
- "@list" :: "args => 'a list" ("[(_)]")
+ "_list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"