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