modernized syntax/translations;
authorwenzelm
Thu Feb 11 21:33:25 2010 +0100 (2010-02-11)
changeset 351090015a0a99ae9
parent 35108 e384e27c229f
child 35110 dc4f61a7918a
modernized syntax/translations;
doc-src/TutorialI/Protocol/Message.thy
src/HOL/Auth/Message.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/MicroJava/DFA/Product.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/DFA/SemilatAlg.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Prolog/Test.thy
     1.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Thu Feb 11 21:31:50 2010 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Thu Feb 11 21:33:25 2010 +0100
     1.3 @@ -82,14 +82,14 @@
     1.4  (*<*)
     1.5  text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
     1.6  syntax
     1.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.8 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.9  
    1.10  syntax (xsymbols)
    1.11 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.12 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.13  
    1.14  translations
    1.15    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.16 -  "{|x, y|}"      == "MPair x y"
    1.17 +  "{|x, y|}"      == "CONST MPair x y"
    1.18  
    1.19  
    1.20  constdefs
     2.1 --- a/src/HOL/Auth/Message.thy	Thu Feb 11 21:31:50 2010 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Thu Feb 11 21:33:25 2010 +0100
     2.3 @@ -51,10 +51,10 @@
     2.4  
     2.5  text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
     2.6  syntax
     2.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     2.8 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     2.9  
    2.10  syntax (xsymbols)
    2.11 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    2.12 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    2.13  
    2.14  translations
    2.15    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
     3.1 --- a/src/HOL/Metis_Examples/Message.thy	Thu Feb 11 21:31:50 2010 +0100
     3.2 +++ b/src/HOL/Metis_Examples/Message.thy	Thu Feb 11 21:33:25 2010 +0100
     3.3 @@ -45,10 +45,10 @@
     3.4  
     3.5  text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
     3.6  syntax
     3.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     3.8 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     3.9  
    3.10  syntax (xsymbols)
    3.11 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    3.12 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    3.13  
    3.14  translations
    3.15    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
     4.1 --- a/src/HOL/MicroJava/DFA/Product.thy	Thu Feb 11 21:31:50 2010 +0100
     4.2 +++ b/src/HOL/MicroJava/DFA/Product.thy	Thu Feb 11 21:33:25 2010 +0100
     4.3 @@ -19,9 +19,10 @@
     4.4   esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
     4.5  "esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
     4.6  
     4.7 -syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
     4.8 +abbreviation
     4.9 +  lesubprod_sntax :: "'a * 'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'a * 'b \<Rightarrow> bool"
    4.10         ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
    4.11 -translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
    4.12 +  where "p <=(rA,rB) q == p <=_(le rA rB) q"
    4.13  
    4.14  lemma unfold_lesub_prod:
    4.15    "p <=(rA,rB) q == le rA rB p q"
     5.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Thu Feb 11 21:31:50 2010 +0100
     5.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Thu Feb 11 21:33:25 2010 +0100
     5.3 @@ -33,9 +33,9 @@
     5.4    "plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
     5.5  (*<*)
     5.6   (* allow \<sub> instead of \<bsub>..\<esub> *)  
     5.7 -  "@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
     5.8 -  "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
     5.9 -  "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    5.10 +  "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    5.11 +  "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
    5.12 +  "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    5.13  
    5.14  translations
    5.15    "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
     6.1 --- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Thu Feb 11 21:31:50 2010 +0100
     6.2 +++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Thu Feb 11 21:33:25 2010 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4    "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
     6.5  
     6.6  consts
     6.7 - "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
     6.8 +  plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
     6.9  primrec
    6.10    "[] ++_f y = y"
    6.11    "(x#xs) ++_f y = xs ++_f (x +_f y)"
     7.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Thu Feb 11 21:31:50 2010 +0100
     7.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Feb 11 21:33:25 2010 +0100
     7.3 @@ -38,7 +38,7 @@
     7.4    "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)
     7.5  
     7.6    "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
     7.7 -(* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
     7.8 +(* "_pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
     7.9    "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)
    7.10  
    7.11    "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
     8.1 --- a/src/HOL/Prolog/Test.thy	Thu Feb 11 21:31:50 2010 +0100
     8.2 +++ b/src/HOL/Prolog/Test.thy	Thu Feb 11 21:33:25 2010 +0100
     8.3 @@ -18,7 +18,7 @@
     8.4  
     8.5  syntax
     8.6    (* list Enumeration *)
     8.7 -  "@list"     :: "args => 'a list"                          ("[(_)]")
     8.8 +  "_list"     :: "args => 'a list"                          ("[(_)]")
     8.9  
    8.10  translations
    8.11    "[x, xs]"     == "x#[xs]"