--- 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 {*
--- 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
--- 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"
--- 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"
--- 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} *}
--- 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
--- 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)
--- 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 *}
--- 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. *}
--- 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 *}
--- 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 *}
--- 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>"
--- 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
--- 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)"