renamed 'const_syntax' to 'notation';
authorwenzelm
Tue Nov 07 11:47:57 2006 +0100 (2006-11-07)
changeset 21210c17fd2df4e9e
parent 21209 dbb8decc36bc
child 21211 5370cfbf3070
renamed 'const_syntax' to 'notation';
src/CTT/Arith.thy
src/CTT/CTT.thy
src/FOL/IFOL.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Induct/Comb.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/Library/Word.thy
src/HOL/Map.thy
src/HOL/Product_Type.thy
src/HOL/Real/HahnBanach/Bounds.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/RealVector.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/CTT/Arith.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/CTT/Arith.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -32,10 +32,10 @@
     1.4    "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
     1.5  
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    mult  (infixr "#\<times>" 70)
    1.10  
    1.11 -const_syntax (HTML output)
    1.12 +notation (HTML output)
    1.13    mult (infixr "#\<times>" 70)
    1.14  
    1.15  
     2.1 --- a/src/CTT/CTT.thy	Tue Nov 07 11:47:56 2006 +0100
     2.2 +++ b/src/CTT/CTT.thy	Tue Nov 07 11:47:57 2006 +0100
     2.3 @@ -70,13 +70,13 @@
     2.4    Times     :: "[t,t]=>t"           (infixr "*" 50)
     2.5    "A * B == SUM _:A. B"
     2.6  
     2.7 -const_syntax (xsymbols)
     2.8 +notation (xsymbols)
     2.9    Elem  ("(_ /\<in> _)" [10,10] 5)
    2.10    Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    2.11    Arrow  (infixr "\<longrightarrow>" 30)
    2.12    Times  (infixr "\<times>" 50)
    2.13  
    2.14 -const_syntax (HTML output)
    2.15 +notation (HTML output)
    2.16    Elem  ("(_ /\<in> _)" [10,10] 5)
    2.17    Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    2.18    Times  (infixr "\<times>" 50)
     3.1 --- a/src/FOL/IFOL.thy	Tue Nov 07 11:47:56 2006 +0100
     3.2 +++ b/src/FOL/IFOL.thy	Tue Nov 07 11:47:57 2006 +0100
     3.3 @@ -48,10 +48,10 @@
     3.4    not_equal     :: "['a, 'a] => o"              (infixl "~=" 50)
     3.5    "x ~= y == ~ (x = y)"
     3.6  
     3.7 -const_syntax (xsymbols)
     3.8 +notation (xsymbols)
     3.9    not_equal  (infixl "\<noteq>" 50)
    3.10  
    3.11 -const_syntax (HTML output)
    3.12 +notation (HTML output)
    3.13    not_equal  (infixl "\<noteq>" 50)
    3.14  
    3.15  syntax (xsymbols)
     4.1 --- a/src/HOL/Fun.thy	Tue Nov 07 11:47:56 2006 +0100
     4.2 +++ b/src/HOL/Fun.thy	Tue Nov 07 11:47:57 2006 +0100
     4.3 @@ -48,10 +48,10 @@
     4.4    comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
     4.5    "f o g == %x. f(g(x))"
     4.6  
     4.7 -const_syntax (xsymbols)
     4.8 +notation (xsymbols)
     4.9    comp  (infixl "\<circ>" 55)
    4.10  
    4.11 -const_syntax (HTML output)
    4.12 +notation (HTML output)
    4.13    comp  (infixl "\<circ>" 55)
    4.14  
    4.15  text{*compatibility*}
     5.1 --- a/src/HOL/HOL.thy	Tue Nov 07 11:47:56 2006 +0100
     5.2 +++ b/src/HOL/HOL.thy	Tue Nov 07 11:47:57 2006 +0100
     5.3 @@ -54,24 +54,24 @@
     5.4  
     5.5  subsubsection {* Additional concrete syntax *}
     5.6  
     5.7 -const_syntax (output)
     5.8 +notation (output)
     5.9    "op ="  (infix "=" 50)
    5.10  
    5.11  abbreviation
    5.12    not_equal     :: "['a, 'a] => bool"               (infixl "~=" 50)
    5.13    "x ~= y == ~ (x = y)"
    5.14  
    5.15 -const_syntax (output)
    5.16 +notation (output)
    5.17    not_equal  (infix "~=" 50)
    5.18  
    5.19 -const_syntax (xsymbols)
    5.20 +notation (xsymbols)
    5.21    Not  ("\<not> _" [40] 40)
    5.22    "op &"  (infixr "\<and>" 35)
    5.23    "op |"  (infixr "\<or>" 30)
    5.24    "op -->"  (infixr "\<longrightarrow>" 25)
    5.25    not_equal  (infix "\<noteq>" 50)
    5.26  
    5.27 -const_syntax (HTML output)
    5.28 +notation (HTML output)
    5.29    Not  ("\<not> _" [40] 40)
    5.30    "op &"  (infixr "\<and>" 35)
    5.31    "op |"  (infixr "\<or>" 30)
    5.32 @@ -81,7 +81,7 @@
    5.33    iff :: "[bool, bool] => bool"  (infixr "<->" 25)
    5.34    "A <-> B == A = B"
    5.35  
    5.36 -const_syntax (xsymbols)
    5.37 +notation (xsymbols)
    5.38    iff  (infixr "\<longleftrightarrow>" 25)
    5.39  
    5.40  
    5.41 @@ -215,12 +215,12 @@
    5.42  in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
    5.43  *} -- {* show types that are presumably too general *}
    5.44  
    5.45 -const_syntax
    5.46 +notation
    5.47    uminus  ("- _" [81] 80)
    5.48  
    5.49 -const_syntax (xsymbols)
    5.50 +notation (xsymbols)
    5.51    abs  ("\<bar>_\<bar>")
    5.52 -const_syntax (HTML output)
    5.53 +notation (HTML output)
    5.54    abs  ("\<bar>_\<bar>")
    5.55  
    5.56  
     6.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Nov 07 11:47:56 2006 +0100
     6.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Nov 07 11:47:57 2006 +0100
     6.3 @@ -25,11 +25,11 @@
     6.4    epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
     6.5    "epsilon = star_n (%n. inverse (real (Suc n)))"
     6.6  
     6.7 -const_syntax (xsymbols)
     6.8 +notation (xsymbols)
     6.9    omega  ("\<omega>")
    6.10    epsilon  ("\<epsilon>")
    6.11  
    6.12 -const_syntax (HTML output)
    6.13 +notation (HTML output)
    6.14    omega  ("\<omega>")
    6.15    epsilon  ("\<epsilon>")
    6.16  
     7.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Nov 07 11:47:56 2006 +0100
     7.2 +++ b/src/HOL/Hyperreal/NSA.thy	Tue Nov 07 11:47:57 2006 +0100
     7.3 @@ -40,10 +40,10 @@
     7.4    galaxy    :: "'a::real_normed_vector star => 'a star set"
     7.5    "galaxy x = {y. (x + -y) \<in> HFinite}"
     7.6  
     7.7 -const_syntax (xsymbols)
     7.8 +notation (xsymbols)
     7.9    approx  (infixl "\<approx>" 50)
    7.10  
    7.11 -const_syntax (HTML output)
    7.12 +notation (HTML output)
    7.13    approx  (infixl "\<approx>" 50)
    7.14  
    7.15  lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
     8.1 --- a/src/HOL/Induct/Comb.thy	Tue Nov 07 11:47:56 2006 +0100
     8.2 +++ b/src/HOL/Induct/Comb.thy	Tue Nov 07 11:47:57 2006 +0100
     8.3 @@ -25,7 +25,7 @@
     8.4                | S
     8.5                | Ap comb comb (infixl "##" 90)
     8.6  
     8.7 -const_syntax (xsymbols)
     8.8 +notation (xsymbols)
     8.9    Ap  (infixl "\<bullet>" 90)
    8.10  
    8.11  
     9.1 --- a/src/HOL/Induct/QuoDataType.thy	Tue Nov 07 11:47:56 2006 +0100
     9.2 +++ b/src/HOL/Induct/QuoDataType.thy	Tue Nov 07 11:47:57 2006 +0100
     9.3 @@ -26,9 +26,9 @@
     9.4    msg_rel :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
     9.5    "X ~~ Y == (X,Y) \<in> msgrel"
     9.6  
     9.7 -const_syntax (xsymbols)
     9.8 +notation (xsymbols)
     9.9    msg_rel  (infixl "\<sim>" 50)
    9.10 -const_syntax (HTML output)
    9.11 +notation (HTML output)
    9.12    msg_rel  (infixl "\<sim>" 50)
    9.13  
    9.14  text{*The first two rules are the desired equations. The next four rules
    10.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 07 11:47:56 2006 +0100
    10.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 07 11:47:57 2006 +0100
    10.3 @@ -24,9 +24,9 @@
    10.4    exp_rel :: "[freeExp, freeExp] => bool"  (infixl "~~" 50)
    10.5    "X ~~ Y == (X,Y) \<in> exprel"
    10.6  
    10.7 -const_syntax (xsymbols)
    10.8 +notation (xsymbols)
    10.9    exp_rel  (infixl "\<sim>" 50)
   10.10 -const_syntax (HTML output)
   10.11 +notation (HTML output)
   10.12    exp_rel  (infixl "\<sim>" 50)
   10.13  
   10.14  text{*The first rule is the desired equation. The next three rules
    11.1 --- a/src/HOL/Integ/IntDef.thy	Tue Nov 07 11:47:56 2006 +0100
    11.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Nov 07 11:47:57 2006 +0100
    11.3 @@ -567,7 +567,7 @@
    11.4    Nats  :: "'a::comm_semiring_1_cancel set"
    11.5    "Nats == range of_nat"
    11.6  
    11.7 -const_syntax (xsymbols)
    11.8 +notation (xsymbols)
    11.9    Nats  ("\<nat>")
   11.10  
   11.11  lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
   11.12 @@ -700,7 +700,7 @@
   11.13    Ints  :: "'a::comm_ring_1 set"
   11.14    "Ints == range of_int"
   11.15  
   11.16 -const_syntax (xsymbols)
   11.17 +notation (xsymbols)
   11.18    Ints  ("\<int>")
   11.19  
   11.20  lemma Ints_0 [simp]: "0 \<in> Ints"
    12.1 --- a/src/HOL/Integ/NatBin.thy	Tue Nov 07 11:47:56 2006 +0100
    12.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Nov 07 11:47:57 2006 +0100
    12.3 @@ -23,10 +23,10 @@
    12.4    square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
    12.5    "x\<twosuperior> == x^2"
    12.6  
    12.7 -const_syntax (latex output)
    12.8 +notation (latex output)
    12.9    square  ("(_\<twosuperior>)" [1000] 999)
   12.10  
   12.11 -const_syntax (HTML output)
   12.12 +notation (HTML output)
   12.13    square  ("(_\<twosuperior>)" [1000] 999)
   12.14  
   12.15  
    13.1 --- a/src/HOL/Lambda/Eta.thy	Tue Nov 07 11:47:56 2006 +0100
    13.2 +++ b/src/HOL/Lambda/Eta.thy	Tue Nov 07 11:47:57 2006 +0100
    13.3 @@ -227,7 +227,7 @@
    13.4    par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
    13.5    "s =e> t == (s, t) \<in> par_eta"
    13.6  
    13.7 -const_syntax (xsymbols)
    13.8 +notation (xsymbols)
    13.9    par_eta_red  (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
   13.10  
   13.11  inductive par_eta
    14.1 --- a/src/HOL/Lambda/Lambda.thy	Tue Nov 07 11:47:56 2006 +0100
    14.2 +++ b/src/HOL/Lambda/Lambda.thy	Tue Nov 07 11:47:57 2006 +0100
    14.3 @@ -62,7 +62,7 @@
    14.4    beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
    14.5    "s ->> t == (s, t) \<in> beta^*"
    14.6  
    14.7 -const_syntax (latex)
    14.8 +notation (latex)
    14.9    beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   14.10    beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
   14.11  
    15.1 --- a/src/HOL/Lambda/Type.thy	Tue Nov 07 11:47:56 2006 +0100
    15.2 +++ b/src/HOL/Lambda/Type.thy	Tue Nov 07 11:47:57 2006 +0100
    15.3 @@ -15,10 +15,10 @@
    15.4    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
    15.5    "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
    15.6  
    15.7 -const_syntax (xsymbols)
    15.8 +notation (xsymbols)
    15.9    shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   15.10  
   15.11 -const_syntax (HTML output)
   15.12 +notation (HTML output)
   15.13    shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
   15.14  
   15.15  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   15.16 @@ -60,10 +60,10 @@
   15.17      ("_ ||- _ : _" [50, 50, 50] 50)
   15.18    "env ||- ts : Ts == typings env ts Ts"
   15.19  
   15.20 -const_syntax (xsymbols)
   15.21 +notation (xsymbols)
   15.22    typing_rel  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   15.23  
   15.24 -const_syntax (latex)
   15.25 +notation (latex)
   15.26    funs  (infixr "\<Rrightarrow>" 200)
   15.27    typings_rel  ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
   15.28  
    16.1 --- a/src/HOL/Lambda/WeakNorm.thy	Tue Nov 07 11:47:56 2006 +0100
    16.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue Nov 07 11:47:57 2006 +0100
    16.3 @@ -365,7 +365,7 @@
    16.4    rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
    16.5    "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
    16.6  
    16.7 -const_syntax (xsymbols)
    16.8 +notation (xsymbols)
    16.9    rtyping_rel  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   16.10  
   16.11  inductive rtyping
    17.1 --- a/src/HOL/Lattice/CompleteLattice.thy	Tue Nov 07 11:47:56 2006 +0100
    17.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Tue Nov 07 11:47:57 2006 +0100
    17.3 @@ -37,7 +37,7 @@
    17.4    Join :: "'a::complete_lattice set \<Rightarrow> 'a"
    17.5    "Join A = (THE sup. is_Sup A sup)"
    17.6  
    17.7 -const_syntax (xsymbols)
    17.8 +notation (xsymbols)
    17.9    Meet  ("\<Sqinter>_" [90] 90)
   17.10    Join  ("\<Squnion>_" [90] 90)
   17.11  
    18.1 --- a/src/HOL/Lattice/Lattice.thy	Tue Nov 07 11:47:56 2006 +0100
    18.2 +++ b/src/HOL/Lattice/Lattice.thy	Tue Nov 07 11:47:57 2006 +0100
    18.3 @@ -30,7 +30,7 @@
    18.4    join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65)
    18.5    "x || y = (THE sup. is_sup x y sup)"
    18.6  
    18.7 -const_syntax (xsymbols)
    18.8 +notation (xsymbols)
    18.9    meet  (infixl "\<sqinter>" 70)
   18.10    join  (infixl "\<squnion>" 65)
   18.11  
    19.1 --- a/src/HOL/Lattice/Orders.thy	Tue Nov 07 11:47:56 2006 +0100
    19.2 +++ b/src/HOL/Lattice/Orders.thy	Tue Nov 07 11:47:57 2006 +0100
    19.3 @@ -21,7 +21,7 @@
    19.4  axclass leq < type
    19.5  consts
    19.6    leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
    19.7 -const_syntax (xsymbols)
    19.8 +notation (xsymbols)
    19.9    leq  (infixl "\<sqsubseteq>" 50)
   19.10  
   19.11  axclass quasi_order < leq
    20.1 --- a/src/HOL/Library/FuncSet.thy	Tue Nov 07 11:47:56 2006 +0100
    20.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Nov 07 11:47:57 2006 +0100
    20.3 @@ -23,7 +23,7 @@
    20.4    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
    20.5    "A -> B == Pi A (%_. B)"
    20.6  
    20.7 -const_syntax (xsymbols)
    20.8 +notation (xsymbols)
    20.9    funcset  (infixr "\<rightarrow>" 60)
   20.10  
   20.11  syntax
    21.1 --- a/src/HOL/Library/Infinite_Set.thy	Tue Nov 07 11:47:56 2006 +0100
    21.2 +++ b/src/HOL/Library/Infinite_Set.thy	Tue Nov 07 11:47:57 2006 +0100
    21.3 @@ -354,11 +354,11 @@
    21.4    Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
    21.5    "Alm_all P = (\<not> (INF x. \<not> P x))"
    21.6  
    21.7 -const_syntax (xsymbols)
    21.8 +notation (xsymbols)
    21.9    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
   21.10    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   21.11  
   21.12 -const_syntax (HTML output)
   21.13 +notation (HTML output)
   21.14    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10)
   21.15    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   21.16  
    22.1 --- a/src/HOL/Library/LaTeXsugar.thy	Tue Nov 07 11:47:56 2006 +0100
    22.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Tue Nov 07 11:47:57 2006 +0100
    22.3 @@ -10,7 +10,7 @@
    22.4  begin
    22.5  
    22.6  (* LOGIC *)
    22.7 -const_syntax (latex output)
    22.8 +notation (latex output)
    22.9    If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
   22.10  
   22.11  syntax (latex output)
   22.12 @@ -52,15 +52,15 @@
   22.13  (* LISTS *)
   22.14  
   22.15  (* Cons *)
   22.16 -const_syntax (latex)
   22.17 +notation (latex)
   22.18    Cons  ("_\<cdot>/_" [66,65] 65)
   22.19  
   22.20  (* length *)
   22.21 -const_syntax (latex output)
   22.22 +notation (latex output)
   22.23    length  ("|_|")
   22.24  
   22.25  (* nth *)
   22.26 -const_syntax (latex output)
   22.27 +notation (latex output)
   22.28    nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
   22.29  
   22.30  (* DUMMY *)
    23.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Nov 07 11:47:56 2006 +0100
    23.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Nov 07 11:47:57 2006 +0100
    23.3 @@ -19,10 +19,10 @@
    23.4  
    23.5  datatype inat = Fin nat | Infty
    23.6  
    23.7 -const_syntax (xsymbols)
    23.8 +notation (xsymbols)
    23.9    Infty  ("\<infinity>")
   23.10  
   23.11 -const_syntax (HTML output)
   23.12 +notation (HTML output)
   23.13    Infty  ("\<infinity>")
   23.14  
   23.15  instance inat :: "{ord, zero}" ..
    24.1 --- a/src/HOL/Library/OptionalSugar.thy	Tue Nov 07 11:47:56 2006 +0100
    24.2 +++ b/src/HOL/Library/OptionalSugar.thy	Tue Nov 07 11:47:57 2006 +0100
    24.3 @@ -17,7 +17,7 @@
    24.4  
    24.5  
    24.6  (* aligning equations *)
    24.7 -const_syntax (tab output)
    24.8 +notation (tab output)
    24.9    "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
   24.10    "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
   24.11  
    25.1 --- a/src/HOL/Library/Word.thy	Tue Nov 07 11:47:56 2006 +0100
    25.2 +++ b/src/HOL/Library/Word.thy	Tue Nov 07 11:47:57 2006 +0100
    25.3 @@ -56,13 +56,13 @@
    25.4    bitor  :: "bit => bit => bit" (infixr "bitor"  30)
    25.5    bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
    25.6  
    25.7 -const_syntax (xsymbols)
    25.8 +notation (xsymbols)
    25.9    bitnot ("\<not>\<^sub>b _" [40] 40)
   25.10    bitand (infixr "\<and>\<^sub>b" 35)
   25.11    bitor  (infixr "\<or>\<^sub>b" 30)
   25.12    bitxor (infixr "\<oplus>\<^sub>b" 30)
   25.13  
   25.14 -const_syntax (HTML output)
   25.15 +notation (HTML output)
   25.16    bitnot ("\<not>\<^sub>b _" [40] 40)
   25.17    bitand (infixr "\<and>\<^sub>b" 35)
   25.18    bitor  (infixr "\<or>\<^sub>b" 30)
    26.1 --- a/src/HOL/Map.thy	Tue Nov 07 11:47:56 2006 +0100
    26.2 +++ b/src/HOL/Map.thy	Tue Nov 07 11:47:57 2006 +0100
    26.3 @@ -26,7 +26,7 @@
    26.4    map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)"  (infixl "o'_m" 55)
    26.5    "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    26.6  
    26.7 -const_syntax (xsymbols)
    26.8 +notation (xsymbols)
    26.9    map_comp  (infixl "\<circ>\<^sub>m" 55)
   26.10  
   26.11  definition
   26.12 @@ -36,7 +36,7 @@
   26.13    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)"  (infixl "|`"  110)
   26.14    "m|`A = (\<lambda>x. if x : A then m x else None)"
   26.15  
   26.16 -const_syntax (latex output)
   26.17 +notation (latex output)
   26.18    restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
   26.19  
   26.20  definition
    27.1 --- a/src/HOL/Product_Type.thy	Tue Nov 07 11:47:56 2006 +0100
    27.2 +++ b/src/HOL/Product_Type.thy	Tue Nov 07 11:47:57 2006 +0100
    27.3 @@ -113,10 +113,10 @@
    27.4    Times :: "['a set, 'b set] => ('a * 'b) set"  (infixr "<*>" 80)
    27.5    "A <*> B == Sigma A (%_. B)"
    27.6  
    27.7 -const_syntax (xsymbols)
    27.8 +notation (xsymbols)
    27.9    Times  (infixr "\<times>" 80)
   27.10  
   27.11 -const_syntax (HTML output)
   27.12 +notation (HTML output)
   27.13    Times  (infixr "\<times>" 80)
   27.14  
   27.15  
    28.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Nov 07 11:47:56 2006 +0100
    28.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Tue Nov 07 11:47:57 2006 +0100
    28.3 @@ -18,7 +18,7 @@
    28.4    the_lub :: "'a::order set \<Rightarrow> 'a"
    28.5    "the_lub A = The (lub A)"
    28.6  
    28.7 -const_syntax (xsymbols)
    28.8 +notation (xsymbols)
    28.9    the_lub  ("\<Squnion>_" [90] 90)
   28.10  
   28.11  lemma the_lub_equality [elim?]:
    29.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Nov 07 11:47:56 2006 +0100
    29.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Nov 07 11:47:57 2006 +0100
    29.3 @@ -22,7 +22,7 @@
    29.4      and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
    29.5      and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
    29.6  
    29.7 -const_syntax (symbols)
    29.8 +notation (symbols)
    29.9    subspace  (infix "\<unlhd>" 50)
   29.10  
   29.11  declare vectorspace.intro [intro?] subspace.intro [intro?]
    30.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Tue Nov 07 11:47:56 2006 +0100
    30.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Tue Nov 07 11:47:57 2006 +0100
    30.3 @@ -18,9 +18,9 @@
    30.4  consts
    30.5    prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)
    30.6  
    30.7 -const_syntax (xsymbols)
    30.8 +notation (xsymbols)
    30.9    prod  (infixr "\<cdot>" 70)
   30.10 -const_syntax (HTML output)
   30.11 +notation (HTML output)
   30.12    prod  (infixr "\<cdot>" 70)
   30.13  
   30.14  
    31.1 --- a/src/HOL/Real/RComplete.thy	Tue Nov 07 11:47:56 2006 +0100
    31.2 +++ b/src/HOL/Real/RComplete.thy	Tue Nov 07 11:47:57 2006 +0100
    31.3 @@ -438,11 +438,11 @@
    31.4    ceiling :: "real => int"
    31.5    "ceiling r = - floor (- r)"
    31.6  
    31.7 -const_syntax (xsymbols)
    31.8 +notation (xsymbols)
    31.9    floor  ("\<lfloor>_\<rfloor>")
   31.10    ceiling  ("\<lceil>_\<rceil>")
   31.11  
   31.12 -const_syntax (HTML output)
   31.13 +notation (HTML output)
   31.14    floor  ("\<lfloor>_\<rfloor>")
   31.15    ceiling  ("\<lceil>_\<rceil>")
   31.16  
    32.1 --- a/src/HOL/Real/RealVector.thy	Tue Nov 07 11:47:56 2006 +0100
    32.2 +++ b/src/HOL/Real/RealVector.thy	Tue Nov 07 11:47:57 2006 +0100
    32.3 @@ -44,7 +44,7 @@
    32.4    divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70)
    32.5    "x /# r == inverse r *# x"
    32.6  
    32.7 -const_syntax (xsymbols)
    32.8 +notation (xsymbols)
    32.9    scaleR (infixr "*\<^sub>R" 75)
   32.10    divideR (infixl "'/\<^sub>R" 70)
   32.11  
   32.12 @@ -253,7 +253,7 @@
   32.13    Reals :: "'a::real_algebra_1 set"
   32.14    "Reals \<equiv> range of_real"
   32.15  
   32.16 -const_syntax (xsymbols)
   32.17 +notation (xsymbols)
   32.18    Reals  ("\<real>")
   32.19  
   32.20  lemma of_real_in_Reals [simp]: "of_real r \<in> Reals"
    33.1 --- a/src/HOL/Relation.thy	Tue Nov 07 11:47:56 2006 +0100
    33.2 +++ b/src/HOL/Relation.thy	Tue Nov 07 11:47:57 2006 +0100
    33.3 @@ -16,7 +16,7 @@
    33.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
    33.5    "r^-1 == {(y, x). (x, y) : r}"
    33.6  
    33.7 -const_syntax (xsymbols)
    33.8 +notation (xsymbols)
    33.9    converse  ("(_\<inverse>)" [1000] 999)
   33.10  
   33.11  definition
    34.1 --- a/src/HOL/Set.thy	Tue Nov 07 11:47:56 2006 +0100
    34.2 +++ b/src/HOL/Set.thy	Tue Nov 07 11:47:57 2006 +0100
    34.3 @@ -37,7 +37,7 @@
    34.4    image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
    34.5    "op :"        :: "'a => 'a set => bool"                -- "membership"
    34.6  
    34.7 -const_syntax
    34.8 +notation
    34.9    "op :"  ("op :")
   34.10    "op :"  ("(_/ : _)" [50, 51] 50)
   34.11  
   34.12 @@ -55,11 +55,11 @@
   34.13  abbreviation
   34.14    "not_mem x A == ~ (x : A)"                  -- "non-membership"
   34.15  
   34.16 -const_syntax
   34.17 +notation
   34.18    not_mem  ("op ~:")
   34.19    not_mem  ("(_/ ~: _)" [50, 51] 50)
   34.20  
   34.21 -const_syntax (xsymbols)
   34.22 +notation (xsymbols)
   34.23    "op Int"  (infixl "\<inter>" 70)
   34.24    "op Un"  (infixl "\<union>" 65)
   34.25    "op :"  ("op \<in>")
   34.26 @@ -69,7 +69,7 @@
   34.27    Union  ("\<Union>_" [90] 90)
   34.28    Inter  ("\<Inter>_" [90] 90)
   34.29  
   34.30 -const_syntax (HTML output)
   34.31 +notation (HTML output)
   34.32    "op Int"  (infixl "\<inter>" 70)
   34.33    "op Un"  (infixl "\<union>" 65)
   34.34    "op :"  ("op \<in>")
   34.35 @@ -83,19 +83,19 @@
   34.36    subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   34.37    "subset_eq == less_eq"
   34.38  
   34.39 -const_syntax (output)
   34.40 +notation (output)
   34.41    subset  ("op <")
   34.42    subset  ("(_/ < _)" [50, 51] 50)
   34.43    subset_eq  ("op <=")
   34.44    subset_eq  ("(_/ <= _)" [50, 51] 50)
   34.45  
   34.46 -const_syntax (xsymbols)
   34.47 +notation (xsymbols)
   34.48    subset  ("op \<subset>")
   34.49    subset  ("(_/ \<subset> _)" [50, 51] 50)
   34.50    subset_eq  ("op \<subseteq>")
   34.51    subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
   34.52  
   34.53 -const_syntax (HTML output)
   34.54 +notation (HTML output)
   34.55    subset  ("op \<subset>")
   34.56    subset  ("(_/ \<subset> _)" [50, 51] 50)
   34.57    subset_eq  ("op \<subseteq>")
    35.1 --- a/src/HOL/Transitive_Closure.thy	Tue Nov 07 11:47:56 2006 +0100
    35.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Nov 07 11:47:57 2006 +0100
    35.3 @@ -40,12 +40,12 @@
    35.4    reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    35.5    "r^= == r \<union> Id"
    35.6  
    35.7 -const_syntax (xsymbols)
    35.8 +notation (xsymbols)
    35.9    rtrancl  ("(_\<^sup>*)" [1000] 999)
   35.10    trancl  ("(_\<^sup>+)" [1000] 999)
   35.11    reflcl  ("(_\<^sup>=)" [1000] 999)
   35.12  
   35.13 -const_syntax (HTML output)
   35.14 +notation (HTML output)
   35.15    rtrancl  ("(_\<^sup>*)" [1000] 999)
   35.16    trancl  ("(_\<^sup>+)" [1000] 999)
   35.17    reflcl  ("(_\<^sup>=)" [1000] 999)
    36.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Tue Nov 07 11:47:56 2006 +0100
    36.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Nov 07 11:47:57 2006 +0100
    36.3 @@ -33,7 +33,7 @@
    36.4    fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_'(C')_)" [64,63] 63)
    36.5    "A(C)s == fsfilter A\<cdot>s"
    36.6  
    36.7 -const_syntax (xsymbols)
    36.8 +notation (xsymbols)
    36.9    fscons'  ("(_\<leadsto>_)"                                                 [66,65] 65)
   36.10    fsfilter'  ("(_\<copyright>_)"                                               [64,63] 63)
   36.11  
    37.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Nov 07 11:47:56 2006 +0100
    37.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Nov 07 11:47:57 2006 +0100
    37.3 @@ -39,7 +39,7 @@
    37.4    fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63)
    37.5    "A(C)s == fsfilter A\<cdot>s"
    37.6  
    37.7 -const_syntax (xsymbols)
    37.8 +notation (xsymbols)
    37.9    fsfilter'  ("(_\<copyright>_)" [64,63] 63)
   37.10  
   37.11  
    38.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 07 11:47:56 2006 +0100
    38.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 07 11:47:57 2006 +0100
    38.3 @@ -223,11 +223,11 @@
    38.4      >> (fn ((loc, mode), args) =>
    38.5          Toplevel.local_theory loc (Specification.abbreviation mode args)));
    38.6  
    38.7 -val const_syntaxP =
    38.8 -  OuterSyntax.command "const_syntax" "constant syntax" K.thy_decl
    38.9 +val notationP =
   38.10 +  OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
   38.11      (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
   38.12      >> (fn ((loc, mode), args) =>
   38.13 -        Toplevel.local_theory loc (Specification.const_syntax mode args)));
   38.14 +        Toplevel.local_theory loc (Specification.notation mode args)));
   38.15  
   38.16  
   38.17  (* constant specifications *)
   38.18 @@ -905,9 +905,9 @@
   38.19    classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   38.20    nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
   38.21    no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
   38.22 -  constdefsP, definitionP, abbreviationP, const_syntaxP,
   38.23 -  axiomatizationP, theoremsP, lemmasP, declareP, globalP, localP,
   38.24 -  hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP,
   38.25 +  constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   38.26 +  theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
   38.27 +  ml_commandP, ml_setupP, setupP, method_setupP,
   38.28    parse_ast_translationP, parse_translationP, print_translationP,
   38.29    typed_print_translationP, print_ast_translationP,
   38.30    token_translationP, oracleP, localeP,