# HG changeset patch # User wenzelm # Date 1162896477 -3600 # Node ID c17fd2df4e9eb5d051ab32d83a74f0811f710b64 # Parent dbb8decc36bc0d8f92c02272b9cec16708933fc3 renamed 'const_syntax' to 'notation'; diff -r dbb8decc36bc -r c17fd2df4e9e src/CTT/Arith.thy --- 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 "#\" 70) -const_syntax (HTML output) +notation (HTML output) mult (infixr "#\" 70) diff -r dbb8decc36bc -r c17fd2df4e9e src/CTT/CTT.thy --- 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 ("(_ /\ _)" [10,10] 5) Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) Arrow (infixr "\" 30) Times (infixr "\" 50) -const_syntax (HTML output) +notation (HTML output) Elem ("(_ /\ _)" [10,10] 5) Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) Times (infixr "\" 50) diff -r dbb8decc36bc -r c17fd2df4e9e src/FOL/IFOL.thy --- 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 "\" 50) -const_syntax (HTML output) +notation (HTML output) not_equal (infixl "\" 50) syntax (xsymbols) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Fun.thy --- 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 "\" 55) -const_syntax (HTML output) +notation (HTML output) comp (infixl "\" 55) text{*compatibility*} diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/HOL.thy --- 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 ("\ _" [40] 40) "op &" (infixr "\" 35) "op |" (infixr "\" 30) "op -->" (infixr "\" 25) not_equal (infix "\" 50) -const_syntax (HTML output) +notation (HTML output) Not ("\ _" [40] 40) "op &" (infixr "\" 35) "op |" (infixr "\" 30) @@ -81,7 +81,7 @@ iff :: "[bool, bool] => bool" (infixr "<->" 25) "A <-> B == A = B" -const_syntax (xsymbols) +notation (xsymbols) iff (infixr "\" 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 ("\_\") -const_syntax (HTML output) +notation (HTML output) abs ("\_\") diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Hyperreal/HyperDef.thy --- 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 ("\") epsilon ("\") -const_syntax (HTML output) +notation (HTML output) omega ("\") epsilon ("\") diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Hyperreal/NSA.thy --- 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) \ HFinite}" -const_syntax (xsymbols) +notation (xsymbols) approx (infixl "\" 50) -const_syntax (HTML output) +notation (HTML output) approx (infixl "\" 50) lemma SReal_def: "Reals == {x. \r. x = hypreal_of_real r}" diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Induct/Comb.thy --- 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 "\" 90) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Induct/QuoDataType.thy --- 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) \ msgrel" -const_syntax (xsymbols) +notation (xsymbols) msg_rel (infixl "\" 50) -const_syntax (HTML output) +notation (HTML output) msg_rel (infixl "\" 50) text{*The first two rules are the desired equations. The next four rules diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Induct/QuoNestedDataType.thy --- 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) \ exprel" -const_syntax (xsymbols) +notation (xsymbols) exp_rel (infixl "\" 50) -const_syntax (HTML output) +notation (HTML output) exp_rel (infixl "\" 50) text{*The first rule is the desired equation. The next three rules diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Integ/IntDef.thy --- 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 ("\") lemma of_nat_in_Nats [simp]: "of_nat n \ Nats" @@ -700,7 +700,7 @@ Ints :: "'a::comm_ring_1 set" "Ints == range of_int" -const_syntax (xsymbols) +notation (xsymbols) Ints ("\") lemma Ints_0 [simp]: "0 \ Ints" diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Integ/NatBin.thy --- 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" ("(_\)" [1000] 999) "x\ == x^2" -const_syntax (latex output) +notation (latex output) square ("(_\)" [1000] 999) -const_syntax (HTML output) +notation (HTML output) square ("(_\)" [1000] 999) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lambda/Eta.thy --- 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) \ par_eta" -const_syntax (xsymbols) +notation (xsymbols) par_eta_red (infixl "\\<^sub>\" 50) inductive par_eta diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lambda/Lambda.thy --- 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) \ beta^*" -const_syntax (latex) +notation (latex) beta_red (infixl "\\<^sub>\" 50) beta_reds (infixl "\\<^sub>\\<^sup>*" 50) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lambda/Type.thy --- 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 \ 'a) \ nat \ 'a \ nat \ 'a" ("_<_:_>" [90, 0, 0] 91) "e = (\j. if j < i then e j else if j = i then a else e (j - 1))" -const_syntax (xsymbols) +notation (xsymbols) shift ("_\_:_\" [90, 0, 0] 91) -const_syntax (HTML output) +notation (HTML output) shift ("_\_:_\" [90, 0, 0] 91) lemma shift_eq [simp]: "i = j \ (e\i:T\) j = T" @@ -60,10 +60,10 @@ ("_ ||- _ : _" [50, 50, 50] 50) "env ||- ts : Ts == typings env ts Ts" -const_syntax (xsymbols) +notation (xsymbols) typing_rel ("_ \ _ : _" [50, 50, 50] 50) -const_syntax (latex) +notation (latex) funs (infixr "\" 200) typings_rel ("_ \ _ : _" [50, 50, 50] 50) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lambda/WeakNorm.thy --- 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 \ type) \ dB \ type \ bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) "e |-\<^sub>R t : T == (e, t, T) \ rtyping" -const_syntax (xsymbols) +notation (xsymbols) rtyping_rel ("_ \\<^sub>R _ : _" [50, 50, 50] 50) inductive rtyping diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lattice/CompleteLattice.thy --- 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 \ 'a" "Join A = (THE sup. is_Sup A sup)" -const_syntax (xsymbols) +notation (xsymbols) Meet ("\_" [90] 90) Join ("\_" [90] 90) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lattice/Lattice.thy --- 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 \ 'a \ 'a" (infixl "||" 65) "x || y = (THE sup. is_sup x y sup)" -const_syntax (xsymbols) +notation (xsymbols) meet (infixl "\" 70) join (infixl "\" 65) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lattice/Orders.thy --- 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 \ 'a \ bool" (infixl "[=" 50) -const_syntax (xsymbols) +notation (xsymbols) leq (infixl "\" 50) axclass quasi_order < leq diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Library/FuncSet.thy --- 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 "\" 60) syntax diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Library/Infinite_Set.thy --- 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 \ bool) \ bool" (binder "MOST " 10) "Alm_all P = (\ (INF x. \ P x))" -const_syntax (xsymbols) +notation (xsymbols) Inf_many (binder "\\<^sub>\" 10) Alm_all (binder "\\<^sub>\" 10) -const_syntax (HTML output) +notation (HTML output) Inf_many (binder "\\<^sub>\" 10) Alm_all (binder "\\<^sub>\" 10) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Library/LaTeXsugar.thy --- 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 ("_\/_" [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 *) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Library/Nat_Infinity.thy --- 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 ("\") -const_syntax (HTML output) +notation (HTML output) Infty ("\") instance inat :: "{ord, zero}" .. diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Library/OptionalSugar.thy --- 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{\ >\\<^raw:}\putisatab\isa{> (_)") diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Library/Word.thy --- 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 ("\\<^sub>b _" [40] 40) bitand (infixr "\\<^sub>b" 35) bitor (infixr "\\<^sub>b" 30) bitxor (infixr "\\<^sub>b" 30) -const_syntax (HTML output) +notation (HTML output) bitnot ("\\<^sub>b _" [40] 40) bitand (infixr "\\<^sub>b" 35) bitor (infixr "\\<^sub>b" 30) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Map.thy --- 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 = (\k. case g k of None \ None | Some v \ f v)" -const_syntax (xsymbols) +notation (xsymbols) map_comp (infixl "\\<^sub>m" 55) definition @@ -36,7 +36,7 @@ restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`" 110) "m|`A = (\x. if x : A then m x else None)" -const_syntax (latex output) +notation (latex output) restrict_map ("_\\<^bsub>_\<^esub>" [111,110] 110) definition diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Product_Type.thy --- 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 "\" 80) -const_syntax (HTML output) +notation (HTML output) Times (infixr "\" 80) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Real/HahnBanach/Bounds.thy --- 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 \ 'a" "the_lub A = The (lub A)" -const_syntax (xsymbols) +notation (xsymbols) the_lub ("\_" [90] 90) lemma the_lub_equality [elim?]: diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Real/HahnBanach/Subspace.thy --- 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 \ U \ y \ U \ x + y \ U" and mult_closed [iff]: "x \ U \ a \ x \ U" -const_syntax (symbols) +notation (symbols) subspace (infix "\" 50) declare vectorspace.intro [intro?] subspace.intro [intro?] diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Real/HahnBanach/VectorSpace.thy --- 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 \ 'a::{plus, minus, zero} \ 'a" (infixr "'(*')" 70) -const_syntax (xsymbols) +notation (xsymbols) prod (infixr "\" 70) -const_syntax (HTML output) +notation (HTML output) prod (infixr "\" 70) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Real/RComplete.thy --- 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 ("\_\") ceiling ("\_\") -const_syntax (HTML output) +notation (HTML output) floor ("\_\") ceiling ("\_\") diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Real/RealVector.thy --- 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 \ real \ '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 \ range of_real" -const_syntax (xsymbols) +notation (xsymbols) Reals ("\") lemma of_real_in_Reals [simp]: "of_real r \ Reals" diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Relation.thy --- 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 ("(_\)" [1000] 999) definition diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Set.thy --- 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 "\" 70) "op Un" (infixl "\" 65) "op :" ("op \") @@ -69,7 +69,7 @@ Union ("\_" [90] 90) Inter ("\_" [90] 90) -const_syntax (HTML output) +notation (HTML output) "op Int" (infixl "\" 70) "op Un" (infixl "\" 65) "op :" ("op \") @@ -83,19 +83,19 @@ subset_eq :: "'a set \ 'a set \ 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 ("(_/ \ _)" [50, 51] 50) subset_eq ("op \") subset_eq ("(_/ \ _)" [50, 51] 50) -const_syntax (HTML output) +notation (HTML output) subset ("op \") subset ("(_/ \ _)" [50, 51] 50) subset_eq ("op \") diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Transitive_Closure.thy --- 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 \ 'a) set => ('a \ 'a) set" ("(_^=)" [1000] 999) "r^= == r \ 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) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOLCF/FOCUS/Fstream.thy --- 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 \ 'a fstream \ 'a fstream" ("(_'(C')_)" [64,63] 63) "A(C)s == fsfilter A\s" -const_syntax (xsymbols) +notation (xsymbols) fscons' ("(_\_)" [66,65] 65) fsfilter' ("(_\_)" [64,63] 63) diff -r dbb8decc36bc -r c17fd2df4e9e src/HOLCF/FOCUS/Fstreams.thy --- 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 \ 'a fstream \ 'a fstream" ("(_'(C')_)" [64,63] 63) "A(C)s == fsfilter A\s" -const_syntax (xsymbols) +notation (xsymbols) fsfilter' ("(_\_)" [64,63] 63) diff -r dbb8decc36bc -r c17fd2df4e9e src/Pure/Isar/isar_syn.ML --- 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,