proper (type_)notation;
authorwenzelm
Tue Mar 02 23:59:54 2010 +0100 (2010-03-02)
changeset 35427ad039d29e01c
parent 35426 c9b9d4fc270d
child 35428 bd7d6f65976e
proper (type_)notation;
src/HOL/Map.thy
src/HOL/Product_Type.thy
src/HOL/UNITY/Union.thy
src/HOLCF/Cfun.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
src/HOLCF/ex/Strict_Fun.thy
src/ZF/Induct/Comb.thy
src/ZF/UNITY/Union.thy
     1.1 --- a/src/HOL/Map.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -12,10 +12,10 @@
     1.4  begin
     1.5  
     1.6  types ('a,'b) "~=>" = "'a => 'b option"  (infixr "~=>" 0)
     1.7 -translations (type) "a ~=> b " <= (type) "a => b option"
     1.8 +translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
     1.9  
    1.10 -syntax (xsymbols)
    1.11 -  "~=>" :: "[type, type] => type"  (infixr "\<rightharpoonup>" 0)
    1.12 +type_notation (xsymbols)
    1.13 +  "~=>"  (infixr "\<rightharpoonup>" 0)
    1.14  
    1.15  abbreviation
    1.16    empty :: "'a ~=> 'b" where
     2.1 --- a/src/HOL/Product_Type.thy	Tue Mar 02 23:56:13 2010 +0100
     2.2 +++ b/src/HOL/Product_Type.thy	Tue Mar 02 23:59:54 2010 +0100
     2.3 @@ -142,10 +142,10 @@
     2.4      by rule+
     2.5  qed
     2.6  
     2.7 -syntax (xsymbols)
     2.8 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
     2.9 -syntax (HTML output)
    2.10 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    2.11 +type_notation (xsymbols)
    2.12 +  "*"  ("(_ \<times>/ _)" [21, 20] 20)
    2.13 +type_notation (HTML output)
    2.14 +  "*"  ("(_ \<times>/ _)" [21, 20] 20)
    2.15  
    2.16  consts
    2.17    Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
     3.1 --- a/src/HOL/UNITY/Union.thy	Tue Mar 02 23:56:13 2010 +0100
     3.2 +++ b/src/HOL/UNITY/Union.thy	Tue Mar 02 23:59:54 2010 +0100
     3.3 @@ -35,21 +35,22 @@
     3.4    safety_prop :: "'a program set => bool"
     3.5      "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
     3.6  
     3.7 +notation
     3.8 +  SKIP  ("\<bottom>") and
     3.9 +  Join  (infixl "\<squnion>" 65)
    3.10 +
    3.11  syntax
    3.12    "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
    3.13    "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
    3.14 +syntax (xsymbols)
    3.15 +  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    3.16 +  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
    3.17  
    3.18  translations
    3.19    "JN x: A. B" == "CONST JOIN A (%x. B)"
    3.20    "JN x y. B" == "JN x. JN y. B"
    3.21    "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
    3.22  
    3.23 -syntax (xsymbols)
    3.24 -  SKIP     :: "'a program"                              ("\<bottom>")
    3.25 -  Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
    3.26 -  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    3.27 -  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
    3.28 -
    3.29  
    3.30  subsection{*SKIP*}
    3.31  
     4.1 --- a/src/HOLCF/Cfun.thy	Tue Mar 02 23:56:13 2010 +0100
     4.2 +++ b/src/HOLCF/Cfun.thy	Tue Mar 02 23:59:54 2010 +0100
     4.3 @@ -23,8 +23,8 @@
     4.4  cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
     4.5  by (simp_all add: Ex_cont adm_cont)
     4.6  
     4.7 -syntax (xsymbols)
     4.8 -  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
     4.9 +type_notation (xsymbols)
    4.10 +  "->"  ("(_ \<rightarrow>/ _)" [1, 0] 0)
    4.11  
    4.12  notation
    4.13    Rep_CFun  ("(_$/_)" [999,1000] 999)
     5.1 --- a/src/HOLCF/Sprod.thy	Tue Mar 02 23:56:13 2010 +0100
     5.2 +++ b/src/HOLCF/Sprod.thy	Tue Mar 02 23:59:54 2010 +0100
     5.3 @@ -22,10 +22,10 @@
     5.4  instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
     5.5  by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
     5.6  
     5.7 -syntax (xsymbols)
     5.8 -  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
     5.9 -syntax (HTML output)
    5.10 -  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    5.11 +type_notation (xsymbols)
    5.12 +  "**"  ("(_ \<otimes>/ _)" [21,20] 20)
    5.13 +type_notation (HTML output)
    5.14 +  "**"  ("(_ \<otimes>/ _)" [21,20] 20)
    5.15  
    5.16  lemma spair_lemma:
    5.17    "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
     6.1 --- a/src/HOLCF/Ssum.thy	Tue Mar 02 23:56:13 2010 +0100
     6.2 +++ b/src/HOLCF/Ssum.thy	Tue Mar 02 23:59:54 2010 +0100
     6.3 @@ -24,10 +24,10 @@
     6.4  instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
     6.5  by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
     6.6  
     6.7 -syntax (xsymbols)
     6.8 -  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
     6.9 -syntax (HTML output)
    6.10 -  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    6.11 +type_notation (xsymbols)
    6.12 +  "++"  ("(_ \<oplus>/ _)" [21, 20] 20)
    6.13 +type_notation (HTML output)
    6.14 +  "++"  ("(_ \<oplus>/ _)" [21, 20] 20)
    6.15  
    6.16  subsection {* Definitions of constructors *}
    6.17  
     7.1 --- a/src/HOLCF/Up.thy	Tue Mar 02 23:56:13 2010 +0100
     7.2 +++ b/src/HOLCF/Up.thy	Tue Mar 02 23:59:54 2010 +0100
     7.3 @@ -14,8 +14,8 @@
     7.4  
     7.5  datatype 'a u = Ibottom | Iup 'a
     7.6  
     7.7 -syntax (xsymbols)
     7.8 -  "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
     7.9 +type_notation (xsymbols)
    7.10 +  u  ("(_\<^sub>\<bottom>)" [1000] 999)
    7.11  
    7.12  primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
    7.13      "Ifup f Ibottom = \<bottom>"
     8.1 --- a/src/HOLCF/ex/Strict_Fun.thy	Tue Mar 02 23:56:13 2010 +0100
     8.2 +++ b/src/HOLCF/ex/Strict_Fun.thy	Tue Mar 02 23:59:54 2010 +0100
     8.3 @@ -12,8 +12,8 @@
     8.4    = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
     8.5  by simp_all
     8.6  
     8.7 -syntax (xsymbols)
     8.8 -  sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0)
     8.9 +type_notation (xsymbols)
    8.10 +  sfun  (infixr "\<rightarrow>!" 0)
    8.11  
    8.12  text {* TODO: Define nice syntax for abstraction, application. *}
    8.13  
     9.1 --- a/src/ZF/Induct/Comb.thy	Tue Mar 02 23:56:13 2010 +0100
     9.2 +++ b/src/ZF/Induct/Comb.thy	Tue Mar 02 23:59:54 2010 +0100
     9.3 @@ -23,6 +23,9 @@
     9.4    | S
     9.5    | app ("p \<in> comb", "q \<in> comb")    (infixl "@@" 90)
     9.6  
     9.7 +notation (xsymbols)
     9.8 +  app  (infixl "\<bullet>" 90)
     9.9 +
    9.10  text {*
    9.11    Inductive definition of contractions, @{text "-1->"} and
    9.12    (multi-step) reductions, @{text "--->"}.
    9.13 @@ -39,9 +42,6 @@
    9.14    contract_multi :: "[i,i] => o"    (infixl "--->" 50)
    9.15    where "p ---> q == <p,q> \<in> contract^*"
    9.16  
    9.17 -syntax (xsymbols)
    9.18 -  "comb.app"    :: "[i, i] => i"             (infixl "\<bullet>" 90)
    9.19 -
    9.20  inductive
    9.21    domains "contract" \<subseteq> "comb \<times> comb"
    9.22    intros
    10.1 --- a/src/ZF/UNITY/Union.thy	Tue Mar 02 23:56:13 2010 +0100
    10.2 +++ b/src/ZF/UNITY/Union.thy	Tue Mar 02 23:59:54 2010 +0100
    10.3 @@ -40,23 +40,22 @@
    10.4    "safety_prop(X) == X\<subseteq>program &
    10.5        SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
    10.6    
    10.7 +notation (xsymbols)
    10.8 +  SKIP  ("\<bottom>") and
    10.9 +  Join  (infixl "\<squnion>" 65)
   10.10 +
   10.11  syntax
   10.12    "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
   10.13    "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
   10.14 +syntax (xsymbols)
   10.15 +  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
   10.16 +  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
   10.17  
   10.18  translations
   10.19    "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
   10.20    "JN x y. B"   == "JN x. JN y. B"
   10.21    "JN x. B"     == "CONST JOIN(CONST state,(%x. B))"
   10.22  
   10.23 -notation (xsymbols)
   10.24 -  SKIP  ("\<bottom>") and
   10.25 -  Join  (infixl "\<squnion>" 65)
   10.26 -
   10.27 -syntax (xsymbols)
   10.28 -  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
   10.29 -  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
   10.30 -
   10.31  
   10.32  subsection{*SKIP*}
   10.33