--- a/src/CTT/Arith.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/CTT/Arith.thy Tue Nov 07 11:47:57 2006 +0100
@@ -32,10 +32,10 @@
"a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
-const_syntax (xsymbols)
+notation (xsymbols)
mult (infixr "#\<times>" 70)
-const_syntax (HTML output)
+notation (HTML output)
mult (infixr "#\<times>" 70)
--- a/src/CTT/CTT.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/CTT/CTT.thy Tue Nov 07 11:47:57 2006 +0100
@@ -70,13 +70,13 @@
Times :: "[t,t]=>t" (infixr "*" 50)
"A * B == SUM _:A. B"
-const_syntax (xsymbols)
+notation (xsymbols)
Elem ("(_ /\<in> _)" [10,10] 5)
Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
Arrow (infixr "\<longrightarrow>" 30)
Times (infixr "\<times>" 50)
-const_syntax (HTML output)
+notation (HTML output)
Elem ("(_ /\<in> _)" [10,10] 5)
Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
Times (infixr "\<times>" 50)
--- a/src/FOL/IFOL.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/FOL/IFOL.thy Tue Nov 07 11:47:57 2006 +0100
@@ -48,10 +48,10 @@
not_equal :: "['a, 'a] => o" (infixl "~=" 50)
"x ~= y == ~ (x = y)"
-const_syntax (xsymbols)
+notation (xsymbols)
not_equal (infixl "\<noteq>" 50)
-const_syntax (HTML output)
+notation (HTML output)
not_equal (infixl "\<noteq>" 50)
syntax (xsymbols)
--- a/src/HOL/Fun.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Fun.thy Tue Nov 07 11:47:57 2006 +0100
@@ -48,10 +48,10 @@
comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "o" 55)
"f o g == %x. f(g(x))"
-const_syntax (xsymbols)
+notation (xsymbols)
comp (infixl "\<circ>" 55)
-const_syntax (HTML output)
+notation (HTML output)
comp (infixl "\<circ>" 55)
text{*compatibility*}
--- a/src/HOL/HOL.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/HOL.thy Tue Nov 07 11:47:57 2006 +0100
@@ -54,24 +54,24 @@
subsubsection {* Additional concrete syntax *}
-const_syntax (output)
+notation (output)
"op =" (infix "=" 50)
abbreviation
not_equal :: "['a, 'a] => bool" (infixl "~=" 50)
"x ~= y == ~ (x = y)"
-const_syntax (output)
+notation (output)
not_equal (infix "~=" 50)
-const_syntax (xsymbols)
+notation (xsymbols)
Not ("\<not> _" [40] 40)
"op &" (infixr "\<and>" 35)
"op |" (infixr "\<or>" 30)
"op -->" (infixr "\<longrightarrow>" 25)
not_equal (infix "\<noteq>" 50)
-const_syntax (HTML output)
+notation (HTML output)
Not ("\<not> _" [40] 40)
"op &" (infixr "\<and>" 35)
"op |" (infixr "\<or>" 30)
@@ -81,7 +81,7 @@
iff :: "[bool, bool] => bool" (infixr "<->" 25)
"A <-> B == A = B"
-const_syntax (xsymbols)
+notation (xsymbols)
iff (infixr "\<longleftrightarrow>" 25)
@@ -215,12 +215,12 @@
in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
*} -- {* show types that are presumably too general *}
-const_syntax
+notation
uminus ("- _" [81] 80)
-const_syntax (xsymbols)
+notation (xsymbols)
abs ("\<bar>_\<bar>")
-const_syntax (HTML output)
+notation (HTML output)
abs ("\<bar>_\<bar>")
--- a/src/HOL/Hyperreal/HyperDef.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Nov 07 11:47:57 2006 +0100
@@ -25,11 +25,11 @@
epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
"epsilon = star_n (%n. inverse (real (Suc n)))"
-const_syntax (xsymbols)
+notation (xsymbols)
omega ("\<omega>")
epsilon ("\<epsilon>")
-const_syntax (HTML output)
+notation (HTML output)
omega ("\<omega>")
epsilon ("\<epsilon>")
--- a/src/HOL/Hyperreal/NSA.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Tue Nov 07 11:47:57 2006 +0100
@@ -40,10 +40,10 @@
galaxy :: "'a::real_normed_vector star => 'a star set"
"galaxy x = {y. (x + -y) \<in> HFinite}"
-const_syntax (xsymbols)
+notation (xsymbols)
approx (infixl "\<approx>" 50)
-const_syntax (HTML output)
+notation (HTML output)
approx (infixl "\<approx>" 50)
lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
--- a/src/HOL/Induct/Comb.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Induct/Comb.thy Tue Nov 07 11:47:57 2006 +0100
@@ -25,7 +25,7 @@
| S
| Ap comb comb (infixl "##" 90)
-const_syntax (xsymbols)
+notation (xsymbols)
Ap (infixl "\<bullet>" 90)
--- a/src/HOL/Induct/QuoDataType.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Induct/QuoDataType.thy Tue Nov 07 11:47:57 2006 +0100
@@ -26,9 +26,9 @@
msg_rel :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
"X ~~ Y == (X,Y) \<in> msgrel"
-const_syntax (xsymbols)
+notation (xsymbols)
msg_rel (infixl "\<sim>" 50)
-const_syntax (HTML output)
+notation (HTML output)
msg_rel (infixl "\<sim>" 50)
text{*The first two rules are the desired equations. The next four rules
--- a/src/HOL/Induct/QuoNestedDataType.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Tue Nov 07 11:47:57 2006 +0100
@@ -24,9 +24,9 @@
exp_rel :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
"X ~~ Y == (X,Y) \<in> exprel"
-const_syntax (xsymbols)
+notation (xsymbols)
exp_rel (infixl "\<sim>" 50)
-const_syntax (HTML output)
+notation (HTML output)
exp_rel (infixl "\<sim>" 50)
text{*The first rule is the desired equation. The next three rules
--- a/src/HOL/Integ/IntDef.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Tue Nov 07 11:47:57 2006 +0100
@@ -567,7 +567,7 @@
Nats :: "'a::comm_semiring_1_cancel set"
"Nats == range of_nat"
-const_syntax (xsymbols)
+notation (xsymbols)
Nats ("\<nat>")
lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
@@ -700,7 +700,7 @@
Ints :: "'a::comm_ring_1 set"
"Ints == range of_int"
-const_syntax (xsymbols)
+notation (xsymbols)
Ints ("\<int>")
lemma Ints_0 [simp]: "0 \<in> Ints"
--- a/src/HOL/Integ/NatBin.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy Tue Nov 07 11:47:57 2006 +0100
@@ -23,10 +23,10 @@
square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999)
"x\<twosuperior> == x^2"
-const_syntax (latex output)
+notation (latex output)
square ("(_\<twosuperior>)" [1000] 999)
-const_syntax (HTML output)
+notation (HTML output)
square ("(_\<twosuperior>)" [1000] 999)
--- a/src/HOL/Lambda/Eta.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lambda/Eta.thy Tue Nov 07 11:47:57 2006 +0100
@@ -227,7 +227,7 @@
par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50)
"s =e> t == (s, t) \<in> par_eta"
-const_syntax (xsymbols)
+notation (xsymbols)
par_eta_red (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
inductive par_eta
--- a/src/HOL/Lambda/Lambda.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lambda/Lambda.thy Tue Nov 07 11:47:57 2006 +0100
@@ -62,7 +62,7 @@
beta_reds :: "[dB, dB] => bool" (infixl "->>" 50)
"s ->> t == (s, t) \<in> beta^*"
-const_syntax (latex)
+notation (latex)
beta_red (infixl "\<rightarrow>\<^sub>\<beta>" 50)
beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
--- a/src/HOL/Lambda/Type.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lambda/Type.thy Tue Nov 07 11:47:57 2006 +0100
@@ -15,10 +15,10 @@
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91)
"e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
-const_syntax (xsymbols)
+notation (xsymbols)
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-const_syntax (HTML output)
+notation (HTML output)
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
@@ -60,10 +60,10 @@
("_ ||- _ : _" [50, 50, 50] 50)
"env ||- ts : Ts == typings env ts Ts"
-const_syntax (xsymbols)
+notation (xsymbols)
typing_rel ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-const_syntax (latex)
+notation (latex)
funs (infixr "\<Rrightarrow>" 200)
typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
--- a/src/HOL/Lambda/WeakNorm.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Tue Nov 07 11:47:57 2006 +0100
@@ -365,7 +365,7 @@
rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
"e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
-const_syntax (xsymbols)
+notation (xsymbols)
rtyping_rel ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
inductive rtyping
--- a/src/HOL/Lattice/CompleteLattice.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Tue Nov 07 11:47:57 2006 +0100
@@ -37,7 +37,7 @@
Join :: "'a::complete_lattice set \<Rightarrow> 'a"
"Join A = (THE sup. is_Sup A sup)"
-const_syntax (xsymbols)
+notation (xsymbols)
Meet ("\<Sqinter>_" [90] 90)
Join ("\<Squnion>_" [90] 90)
--- a/src/HOL/Lattice/Lattice.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lattice/Lattice.thy Tue Nov 07 11:47:57 2006 +0100
@@ -30,7 +30,7 @@
join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65)
"x || y = (THE sup. is_sup x y sup)"
-const_syntax (xsymbols)
+notation (xsymbols)
meet (infixl "\<sqinter>" 70)
join (infixl "\<squnion>" 65)
--- a/src/HOL/Lattice/Orders.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lattice/Orders.thy Tue Nov 07 11:47:57 2006 +0100
@@ -21,7 +21,7 @@
axclass leq < type
consts
leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
-const_syntax (xsymbols)
+notation (xsymbols)
leq (infixl "\<sqsubseteq>" 50)
axclass quasi_order < leq
--- a/src/HOL/Library/FuncSet.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/FuncSet.thy Tue Nov 07 11:47:57 2006 +0100
@@ -23,7 +23,7 @@
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60)
"A -> B == Pi A (%_. B)"
-const_syntax (xsymbols)
+notation (xsymbols)
funcset (infixr "\<rightarrow>" 60)
syntax
--- a/src/HOL/Library/Infinite_Set.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Tue Nov 07 11:47:57 2006 +0100
@@ -354,11 +354,11 @@
Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "MOST " 10)
"Alm_all P = (\<not> (INF x. \<not> P x))"
-const_syntax (xsymbols)
+notation (xsymbols)
Inf_many (binder "\<exists>\<^sub>\<infinity>" 10)
Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
-const_syntax (HTML output)
+notation (HTML output)
Inf_many (binder "\<exists>\<^sub>\<infinity>" 10)
Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
--- a/src/HOL/Library/LaTeXsugar.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Tue Nov 07 11:47:57 2006 +0100
@@ -10,7 +10,7 @@
begin
(* LOGIC *)
-const_syntax (latex output)
+notation (latex output)
If ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
syntax (latex output)
@@ -52,15 +52,15 @@
(* LISTS *)
(* Cons *)
-const_syntax (latex)
+notation (latex)
Cons ("_\<cdot>/_" [66,65] 65)
(* length *)
-const_syntax (latex output)
+notation (latex output)
length ("|_|")
(* nth *)
-const_syntax (latex output)
+notation (latex output)
nth ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
(* DUMMY *)
--- a/src/HOL/Library/Nat_Infinity.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy Tue Nov 07 11:47:57 2006 +0100
@@ -19,10 +19,10 @@
datatype inat = Fin nat | Infty
-const_syntax (xsymbols)
+notation (xsymbols)
Infty ("\<infinity>")
-const_syntax (HTML output)
+notation (HTML output)
Infty ("\<infinity>")
instance inat :: "{ord, zero}" ..
--- a/src/HOL/Library/OptionalSugar.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Tue Nov 07 11:47:57 2006 +0100
@@ -17,7 +17,7 @@
(* aligning equations *)
-const_syntax (tab output)
+notation (tab output)
"op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
"==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
--- a/src/HOL/Library/Word.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Library/Word.thy Tue Nov 07 11:47:57 2006 +0100
@@ -56,13 +56,13 @@
bitor :: "bit => bit => bit" (infixr "bitor" 30)
bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
-const_syntax (xsymbols)
+notation (xsymbols)
bitnot ("\<not>\<^sub>b _" [40] 40)
bitand (infixr "\<and>\<^sub>b" 35)
bitor (infixr "\<or>\<^sub>b" 30)
bitxor (infixr "\<oplus>\<^sub>b" 30)
-const_syntax (HTML output)
+notation (HTML output)
bitnot ("\<not>\<^sub>b _" [40] 40)
bitand (infixr "\<and>\<^sub>b" 35)
bitor (infixr "\<or>\<^sub>b" 30)
--- a/src/HOL/Map.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Map.thy Tue Nov 07 11:47:57 2006 +0100
@@ -26,7 +26,7 @@
map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
"f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
-const_syntax (xsymbols)
+notation (xsymbols)
map_comp (infixl "\<circ>\<^sub>m" 55)
definition
@@ -36,7 +36,7 @@
restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`" 110)
"m|`A = (\<lambda>x. if x : A then m x else None)"
-const_syntax (latex output)
+notation (latex output)
restrict_map ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
definition
--- a/src/HOL/Product_Type.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Product_Type.thy Tue Nov 07 11:47:57 2006 +0100
@@ -113,10 +113,10 @@
Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80)
"A <*> B == Sigma A (%_. B)"
-const_syntax (xsymbols)
+notation (xsymbols)
Times (infixr "\<times>" 80)
-const_syntax (HTML output)
+notation (HTML output)
Times (infixr "\<times>" 80)
--- a/src/HOL/Real/HahnBanach/Bounds.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Tue Nov 07 11:47:57 2006 +0100
@@ -18,7 +18,7 @@
the_lub :: "'a::order set \<Rightarrow> 'a"
"the_lub A = The (lub A)"
-const_syntax (xsymbols)
+notation (xsymbols)
the_lub ("\<Squnion>_" [90] 90)
lemma the_lub_equality [elim?]:
--- a/src/HOL/Real/HahnBanach/Subspace.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Nov 07 11:47:57 2006 +0100
@@ -22,7 +22,7 @@
and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
-const_syntax (symbols)
+notation (symbols)
subspace (infix "\<unlhd>" 50)
declare vectorspace.intro [intro?] subspace.intro [intro?]
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Nov 07 11:47:57 2006 +0100
@@ -18,9 +18,9 @@
consts
prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
-const_syntax (xsymbols)
+notation (xsymbols)
prod (infixr "\<cdot>" 70)
-const_syntax (HTML output)
+notation (HTML output)
prod (infixr "\<cdot>" 70)
--- a/src/HOL/Real/RComplete.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Real/RComplete.thy Tue Nov 07 11:47:57 2006 +0100
@@ -438,11 +438,11 @@
ceiling :: "real => int"
"ceiling r = - floor (- r)"
-const_syntax (xsymbols)
+notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
ceiling ("\<lceil>_\<rceil>")
-const_syntax (HTML output)
+notation (HTML output)
floor ("\<lfloor>_\<rfloor>")
ceiling ("\<lceil>_\<rceil>")
--- a/src/HOL/Real/RealVector.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Real/RealVector.thy Tue Nov 07 11:47:57 2006 +0100
@@ -44,7 +44,7 @@
divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70)
"x /# r == inverse r *# x"
-const_syntax (xsymbols)
+notation (xsymbols)
scaleR (infixr "*\<^sub>R" 75)
divideR (infixl "'/\<^sub>R" 70)
@@ -253,7 +253,7 @@
Reals :: "'a::real_algebra_1 set"
"Reals \<equiv> range of_real"
-const_syntax (xsymbols)
+notation (xsymbols)
Reals ("\<real>")
lemma of_real_in_Reals [simp]: "of_real r \<in> Reals"
--- a/src/HOL/Relation.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Relation.thy Tue Nov 07 11:47:57 2006 +0100
@@ -16,7 +16,7 @@
converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999)
"r^-1 == {(y, x). (x, y) : r}"
-const_syntax (xsymbols)
+notation (xsymbols)
converse ("(_\<inverse>)" [1000] 999)
definition
--- a/src/HOL/Set.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Set.thy Tue Nov 07 11:47:57 2006 +0100
@@ -37,7 +37,7 @@
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90)
"op :" :: "'a => 'a set => bool" -- "membership"
-const_syntax
+notation
"op :" ("op :")
"op :" ("(_/ : _)" [50, 51] 50)
@@ -55,11 +55,11 @@
abbreviation
"not_mem x A == ~ (x : A)" -- "non-membership"
-const_syntax
+notation
not_mem ("op ~:")
not_mem ("(_/ ~: _)" [50, 51] 50)
-const_syntax (xsymbols)
+notation (xsymbols)
"op Int" (infixl "\<inter>" 70)
"op Un" (infixl "\<union>" 65)
"op :" ("op \<in>")
@@ -69,7 +69,7 @@
Union ("\<Union>_" [90] 90)
Inter ("\<Inter>_" [90] 90)
-const_syntax (HTML output)
+notation (HTML output)
"op Int" (infixl "\<inter>" 70)
"op Un" (infixl "\<union>" 65)
"op :" ("op \<in>")
@@ -83,19 +83,19 @@
subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
"subset_eq == less_eq"
-const_syntax (output)
+notation (output)
subset ("op <")
subset ("(_/ < _)" [50, 51] 50)
subset_eq ("op <=")
subset_eq ("(_/ <= _)" [50, 51] 50)
-const_syntax (xsymbols)
+notation (xsymbols)
subset ("op \<subset>")
subset ("(_/ \<subset> _)" [50, 51] 50)
subset_eq ("op \<subseteq>")
subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
-const_syntax (HTML output)
+notation (HTML output)
subset ("op \<subset>")
subset ("(_/ \<subset> _)" [50, 51] 50)
subset_eq ("op \<subseteq>")
--- a/src/HOL/Transitive_Closure.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Transitive_Closure.thy Tue Nov 07 11:47:57 2006 +0100
@@ -40,12 +40,12 @@
reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999)
"r^= == r \<union> Id"
-const_syntax (xsymbols)
+notation (xsymbols)
rtrancl ("(_\<^sup>*)" [1000] 999)
trancl ("(_\<^sup>+)" [1000] 999)
reflcl ("(_\<^sup>=)" [1000] 999)
-const_syntax (HTML output)
+notation (HTML output)
rtrancl ("(_\<^sup>*)" [1000] 999)
trancl ("(_\<^sup>+)" [1000] 999)
reflcl ("(_\<^sup>=)" [1000] 999)
--- a/src/HOLCF/FOCUS/Fstream.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Tue Nov 07 11:47:57 2006 +0100
@@ -33,7 +33,7 @@
fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
"A(C)s == fsfilter A\<cdot>s"
-const_syntax (xsymbols)
+notation (xsymbols)
fscons' ("(_\<leadsto>_)" [66,65] 65)
fsfilter' ("(_\<copyright>_)" [64,63] 63)
--- a/src/HOLCF/FOCUS/Fstreams.thy Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Tue Nov 07 11:47:57 2006 +0100
@@ -39,7 +39,7 @@
fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
"A(C)s == fsfilter A\<cdot>s"
-const_syntax (xsymbols)
+notation (xsymbols)
fsfilter' ("(_\<copyright>_)" [64,63] 63)
--- a/src/Pure/Isar/isar_syn.ML Tue Nov 07 11:47:56 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Nov 07 11:47:57 2006 +0100
@@ -223,11 +223,11 @@
>> (fn ((loc, mode), args) =>
Toplevel.local_theory loc (Specification.abbreviation mode args)));
-val const_syntaxP =
- OuterSyntax.command "const_syntax" "constant syntax" K.thy_decl
+val notationP =
+ OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
(P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
>> (fn ((loc, mode), args) =>
- Toplevel.local_theory loc (Specification.const_syntax mode args)));
+ Toplevel.local_theory loc (Specification.notation mode args)));
(* constant specifications *)
@@ -905,9 +905,9 @@
classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
- constdefsP, definitionP, abbreviationP, const_syntaxP,
- axiomatizationP, theoremsP, lemmasP, declareP, globalP, localP,
- hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP,
+ constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
+ theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
+ ml_commandP, ml_setupP, setupP, method_setupP,
parse_ast_translationP, parse_translationP, print_translationP,
typed_print_translationP, print_ast_translationP,
token_translationP, oracleP, localeP,