# HG changeset patch
# User wenzelm
# Date 1451507018 -3600
# Node ID b66d2ca1f907d1337e3429c9f91a46d582aadd1c
# Parent  4d9518c3d031cff68adb1aa7fbd6c99acd7ec874
clarified print modes;

diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -15,16 +15,16 @@
 
 definition "cfun = {f::'a => 'b. cont f}"
 
-cpodef ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
+cpodef ('a, 'b) cfun ("(_ \<rightarrow>/ _)" [1, 0] 0) = "cfun :: ('a => 'b) set"
   unfolding cfun_def by (auto intro: cont_const adm_cont)
 
-type_notation (xsymbols)
-  cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
+type_notation (ASCII)
+  cfun  (infixr "->" 0)
+
+notation (ASCII)
+  Rep_cfun  ("(_$/_)" [999,1000] 999)
 
 notation
-  Rep_cfun  ("(_$/_)" [999,1000] 999)
-
-notation (xsymbols)
   Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
 
 
@@ -45,10 +45,10 @@
 
 text {* Syntax for nested abstractions *}
 
-syntax
+syntax (ASCII)
   "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
 
-syntax (xsymbols)
+syntax
   "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
 
 parse_ast_translation {*
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -119,12 +119,10 @@
 
 subsection {* Type definition *}
 
-typedef 'a convex_pd =
+typedef 'a convex_pd  ("('(_')\<natural>)") =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
-type_notation (xsymbols) convex_pd ("('(_')\<natural>)")
-
 instantiation convex_pd :: (bifinite) below
 begin
 
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -29,16 +29,16 @@
   "<> == \<bottom>"
 
 abbreviation
-  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_~>_)"    [66,65] 65) where
-  "a~>s == fscons a\<cdot>s"
+  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_\<leadsto>_)" [66,65] 65) where
+  "a\<leadsto>s == fscons a\<cdot>s"
 
 abbreviation
-  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_'(C')_)" [64,63] 63) where
-  "A(C)s == fsfilter A\<cdot>s"
+  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_\<copyright>_)" [64,63] 63) where
+  "A\<copyright>s == fsfilter A\<cdot>s"
 
-notation (xsymbols)
-  fscons'  ("(_\<leadsto>_)"                                                 [66,65] 65) and
-  fsfilter'  ("(_\<copyright>_)"                                               [64,63] 63)
+notation (ASCII)
+  fscons'  ("(_~>_)" [66,65] 65) and
+  fsfilter'  ("(_'(C')_)" [64,63] 63)
 
 
 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -44,11 +44,11 @@
   "<> == \<bottom>"
 
 abbreviation
-  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_'(C')_)" [64,63] 63) where
-  "A(C)s == fsfilter A\<cdot>s"
+  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_\<copyright>_)" [64,63] 63) where
+  "A\<copyright>s == fsfilter A\<cdot>s"
 
-notation (xsymbols)
-  fsfilter'  ("(_\<copyright>_)" [64,63] 63)
+notation (ASCII)
+  fsfilter'  ("(_'(C')_)" [64,63] 63)
 
 
 lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Fix.thy
--- a/src/HOL/HOLCF/Fix.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Fix.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -49,11 +49,11 @@
 text {* Binder syntax for @{term fix} *}
 
 abbreviation
-  fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "FIX " 10) where
+  fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "\<mu> " 10) where
   "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
 
-notation (xsymbols)
-  fix_syn  (binder "\<mu> " 10)
+notation (ASCII)
+  fix_syn  (binder "FIX " 10)
 
 text {* Properties of @{term fix} *}
 
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -74,12 +74,10 @@
 
 subsection {* Type definition *}
 
-typedef 'a lower_pd =
+typedef 'a lower_pd  ("('(_')\<flat>)") =
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (rule lower_le.ex_ideal)
 
-type_notation (xsymbols) lower_pd ("('(_')\<flat>)")
-
 instantiation lower_pd :: (bifinite) below
 begin
 
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -143,12 +143,9 @@
   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
 begin
 
-definition bottom :: "'a"
+definition bottom :: "'a"  ("\<bottom>")
   where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
 
-notation (xsymbols)
-  bottom ("\<bottom>")
-
 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
 unfolding bottom_def
 apply (rule the1I2)
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Porder.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -17,18 +17,18 @@
   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
-notation
+notation (ASCII)
   below (infix "<<" 50)
 
-notation (xsymbols)
+notation
   below (infix "\<sqsubseteq>" 50)
 
 abbreviation
-  not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "~<<" 50)
+  not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<notsqsubseteq>" 50)
   where "not_below x y \<equiv> \<not> below x y"
 
-notation (xsymbols)
-  not_below (infix "\<notsqsubseteq>" 50)
+notation (ASCII)
+  not_below  (infix "~<<" 50)
 
 lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   by (rule subst)
@@ -112,10 +112,10 @@
 
 end
 
-syntax
+syntax (ASCII)
   "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10)
 
-syntax (xsymbols)
+syntax
   "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10)
 
 translations
@@ -125,11 +125,11 @@
 begin
 
 abbreviation
-  Lub  (binder "LUB " 10) where
-  "LUB n. t n == lub (range t)"
+  Lub  (binder "\<Squnion>" 10) where
+  "\<Squnion>n. t n == lub (range t)"
 
-notation (xsymbols)
-  Lub  (binder "\<Squnion>" 10)
+notation (ASCII)
+  Lub  (binder "LUB " 10)
 
 text {* access to some definition as inference rule *}
 
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Sfun.thy
--- a/src/HOL/HOLCF/Sfun.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -8,12 +8,12 @@
 imports Cfun
 begin
 
-pcpodef ('a, 'b) sfun (infixr "->!" 0)
+pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0)
   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
 by simp_all
 
-type_notation (xsymbols)
-  sfun  (infixr "\<rightarrow>!" 0)
+type_notation (ASCII)
+  sfun  (infixr "->!" 0)
 
 text {* TODO: Define nice syntax for abstraction, application. *}
 
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Sprod.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -15,14 +15,14 @@
 
 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a, 'b) sprod  ("(_ \<otimes>/ _)" [21,20] 20) = "sprod :: ('a \<times> 'b) set"
   unfolding sprod_def by simp_all
 
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
 
-type_notation (xsymbols)
-  sprod  ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (ASCII)
+  sprod  (infixr "**" 20)
 
 
 subsection {* Definitions of constants *}
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Ssum.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -19,14 +19,14 @@
       (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
       (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum  ("(_ \<oplus>/ _)" [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
   unfolding ssum_def by simp_all
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
 
-type_notation (xsymbols)
-  ssum  ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (ASCII)
+  ssum  (infixr "++" 10)
 
 
 subsection {* Definitions of constructors *}
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Up.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -13,10 +13,7 @@
 
 subsection {* Definition of new type for lifting *}
 
-datatype 'a u = Ibottom | Iup 'a
-
-type_notation (xsymbols)
-  u  ("(_\<^sub>\<bottom>)" [1000] 999)
+datatype 'a u  ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a
 
 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
     "Ifup f Ibottom = \<bottom>"
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -72,12 +72,10 @@
 
 subsection {* Type definition *}
 
-typedef 'a upper_pd =
+typedef 'a upper_pd  ("('(_')\<sharp>)") =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
-type_notation (xsymbols) upper_pd ("('(_')\<sharp>)")
-
 instantiation upper_pd :: (bifinite) below
 begin
 
diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -104,13 +104,13 @@
 
 syntax
   "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
-  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ =>/ _)" 10)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ \<Rightarrow>/ _)" 10)
   ""            :: "Case_syn => Cases_syn"               ("_")
   "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
   "_strip_positions" :: "'a => Case_pat"                 ("_")
 
-syntax (xsymbols)
-  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ \<Rightarrow>/ _)" 10)
+syntax (ASCII)
+  "_Case1"      :: "[Case_pat, 'b] => Case_syn"          ("(2_ =>/ _)" 10)
 
 translations
   "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"