# HG changeset patch
# User wenzelm
# Date 1265920405 -3600
# Node ID 0015a0a99ae9f202a3df944fd337ea6012e3d349
# Parent  e384e27c229fd5dae86186bc9ea5ab42acaf233b
modernized syntax/translations;

diff -r e384e27c229f -r 0015a0a99ae9 doc-src/TutorialI/Protocol/Message.thy
--- 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
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/Auth/Message.thy
--- 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|}|}"
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/Metis_Examples/Message.thy
--- 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|}|}"
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/MicroJava/DFA/Product.thy
--- 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"
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/MicroJava/DFA/Semilat.thy
--- 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"
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/MicroJava/DFA/SemilatAlg.thy
--- 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)"
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/Modelcheck/MuckeSyn.thy
--- 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"             ("_ _")
diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/Prolog/Test.thy
--- 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]"