# HG changeset patch
# User wenzelm
# Date 1267570794 -3600
# Node ID ad039d29e01c38c1a265a578ea080dcae86e1689
# Parent  c9b9d4fc270d8a069e28c1af5f18af85a93e0275
proper (type_)notation;

diff -r c9b9d4fc270d -r ad039d29e01c src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOL/Map.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -12,10 +12,10 @@
 begin
 
 types ('a,'b) "~=>" = "'a => 'b option"  (infixr "~=>" 0)
-translations (type) "a ~=> b " <= (type) "a => b option"
+translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
 
-syntax (xsymbols)
-  "~=>" :: "[type, type] => type"  (infixr "\<rightharpoonup>" 0)
+type_notation (xsymbols)
+  "~=>"  (infixr "\<rightharpoonup>" 0)
 
 abbreviation
   empty :: "'a ~=> 'b" where
diff -r c9b9d4fc270d -r ad039d29e01c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOL/Product_Type.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -142,10 +142,10 @@
     by rule+
 qed
 
-syntax (xsymbols)
-  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
-syntax (HTML output)
-  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+  "*"  ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (HTML output)
+  "*"  ("(_ \<times>/ _)" [21, 20] 20)
 
 consts
   Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
diff -r c9b9d4fc270d -r ad039d29e01c src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOL/UNITY/Union.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -35,21 +35,22 @@
   safety_prop :: "'a program set => bool"
     "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
 
+notation
+  SKIP  ("\<bottom>") and
+  Join  (infixl "\<squnion>" 65)
+
 syntax
   "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
   "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
+  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
 
 translations
   "JN x: A. B" == "CONST JOIN A (%x. B)"
   "JN x y. B" == "JN x. JN y. B"
   "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
 
-syntax (xsymbols)
-  SKIP     :: "'a program"                              ("\<bottom>")
-  Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
-  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
-  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
-
 
 subsection{*SKIP*}
 
diff -r c9b9d4fc270d -r ad039d29e01c src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOLCF/Cfun.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -23,8 +23,8 @@
 cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
 by (simp_all add: Ex_cont adm_cont)
 
-syntax (xsymbols)
-  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
+type_notation (xsymbols)
+  "->"  ("(_ \<rightarrow>/ _)" [1, 0] 0)
 
 notation
   Rep_CFun  ("(_$/_)" [999,1000] 999)
diff -r c9b9d4fc270d -r ad039d29e01c src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOLCF/Sprod.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -22,10 +22,10 @@
 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
 
-syntax (xsymbols)
-  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
-syntax (HTML output)
-  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (xsymbols)
+  "**"  ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (HTML output)
+  "**"  ("(_ \<otimes>/ _)" [21,20] 20)
 
 lemma spair_lemma:
   "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
diff -r c9b9d4fc270d -r ad039d29e01c src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOLCF/Ssum.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -24,10 +24,10 @@
 instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
 
-syntax (xsymbols)
-  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
-syntax (HTML output)
-  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+  "++"  ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (HTML output)
+  "++"  ("(_ \<oplus>/ _)" [21, 20] 20)
 
 subsection {* Definitions of constructors *}
 
diff -r c9b9d4fc270d -r ad039d29e01c src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOLCF/Up.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -14,8 +14,8 @@
 
 datatype 'a u = Ibottom | Iup 'a
 
-syntax (xsymbols)
-  "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
+type_notation (xsymbols)
+  u  ("(_\<^sub>\<bottom>)" [1000] 999)
 
 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
     "Ifup f Ibottom = \<bottom>"
diff -r c9b9d4fc270d -r ad039d29e01c src/HOLCF/ex/Strict_Fun.thy
--- a/src/HOLCF/ex/Strict_Fun.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/HOLCF/ex/Strict_Fun.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -12,8 +12,8 @@
   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
 by simp_all
 
-syntax (xsymbols)
-  sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0)
+type_notation (xsymbols)
+  sfun  (infixr "\<rightarrow>!" 0)
 
 text {* TODO: Define nice syntax for abstraction, application. *}
 
diff -r c9b9d4fc270d -r ad039d29e01c src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/ZF/Induct/Comb.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -23,6 +23,9 @@
   | S
   | app ("p \<in> comb", "q \<in> comb")    (infixl "@@" 90)
 
+notation (xsymbols)
+  app  (infixl "\<bullet>" 90)
+
 text {*
   Inductive definition of contractions, @{text "-1->"} and
   (multi-step) reductions, @{text "--->"}.
@@ -39,9 +42,6 @@
   contract_multi :: "[i,i] => o"    (infixl "--->" 50)
   where "p ---> q == <p,q> \<in> contract^*"
 
-syntax (xsymbols)
-  "comb.app"    :: "[i, i] => i"             (infixl "\<bullet>" 90)
-
 inductive
   domains "contract" \<subseteq> "comb \<times> comb"
   intros
diff -r c9b9d4fc270d -r ad039d29e01c src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Tue Mar 02 23:56:13 2010 +0100
+++ b/src/ZF/UNITY/Union.thy	Tue Mar 02 23:59:54 2010 +0100
@@ -40,23 +40,22 @@
   "safety_prop(X) == X\<subseteq>program &
       SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
   
+notation (xsymbols)
+  SKIP  ("\<bottom>") and
+  Join  (infixl "\<squnion>" 65)
+
 syntax
   "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
   "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
+  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
 
 translations
   "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
   "JN x y. B"   == "JN x. JN y. B"
   "JN x. B"     == "CONST JOIN(CONST state,(%x. B))"
 
-notation (xsymbols)
-  SKIP  ("\<bottom>") and
-  Join  (infixl "\<squnion>" 65)
-
-syntax (xsymbols)
-  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
-  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
-
 
 subsection{*SKIP*}