--- a/src/FOL/IFOL.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/FOL/IFOL.thy Fri Nov 09 00:09:47 2001 +0100
@@ -47,18 +47,14 @@
translations
"x ~= y" == "~ (x = y)"
-syntax (symbols)
+syntax (xsymbols)
Not :: "o => o" ("\<not> _" [40] 40)
"op &" :: "[o, o] => o" (infixr "\<and>" 35)
"op |" :: "[o, o] => o" (infixr "\<or>" 30)
- "op -->" :: "[o, o] => o" (infixr "\<midarrow>\<rightarrow>" 25)
- "op <->" :: "[o, o] => o" (infixr "\<leftarrow>\<rightarrow>" 25)
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
"op ~=" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
-
-syntax (xsymbols)
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
--- a/src/HOL/Finite.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Finite.thy Fri Nov 09 00:09:47 2001 +0100
@@ -63,7 +63,7 @@
syntax
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_:_. _" [0, 51, 10] 10)
-syntax (symbols)
+syntax (xsymbols)
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10)
translations
"\\<Sum>i:A. b" == "setsum (%i. b) A" (* Beware of argument permutation! *)
--- a/src/HOL/Fun.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Fun.thy Fri Nov 09 00:09:47 2001 +0100
@@ -46,7 +46,7 @@
inj_on :: ['a => 'b, 'a set] => bool
"inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
-syntax (symbols)
+syntax (xsymbols)
"op o" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\\<circ>" 55)
syntax
@@ -79,7 +79,7 @@
(*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
-syntax (symbols)
+syntax (xsymbols)
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<Pi> _\\<in>_./ _)" 10)
translations
--- a/src/HOL/GroupTheory/Group.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/GroupTheory/Group.thy Fri Nov 09 00:09:47 2001 +0100
@@ -9,7 +9,7 @@
Group = Main +
(*Giving funcset the nice arrow syntax \\<rightarrow> *)
-syntax (symbols)
+syntax (xsymbols)
"op funcset" :: "['a set, 'b set] => ('a => 'b) set" (infixr "\\<rightarrow>" 60)
@@ -21,7 +21,7 @@
record 'a grouptype = 'a semigrouptype +
inverse :: "'a => 'a"
unit :: "'a"
-(* This should be obsolete, if records will allow the promised syntax *)
+
syntax
"@carrier" :: "'a semigrouptype => 'a set" ("_ .<cr>" [10] 10)
"@bin_op" :: "'a semigrouptype => (['a, 'a] => 'a)" ("_ .<f>" [10] 10)
--- a/src/HOL/HOL.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/HOL.thy Fri Nov 09 00:09:47 2001 +0100
@@ -78,11 +78,11 @@
"=" :: "['a, 'a] => bool" (infix 50)
"~=" :: "['a, 'a] => bool" (infix 50)
-syntax (symbols)
+syntax (xsymbols)
Not :: "bool => bool" ("\<not> _" [40] 40)
"op &" :: "[bool, bool] => bool" (infixr "\<and>" 35)
"op |" :: "[bool, bool] => bool" (infixr "\<or>" 30)
- "op -->" :: "[bool, bool] => bool" (infixr "\<midarrow>\<rightarrow>" 25)
+ "op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25)
"op ~=" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10)
@@ -90,12 +90,9 @@
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*)
-syntax (symbols output)
+syntax (xsymbols output)
"op ~=" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
-syntax (xsymbols)
- "op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25)
-
syntax (HTML output)
Not :: "bool => bool" ("\<not> _" [40] 40)
@@ -353,7 +350,7 @@
local
-syntax (symbols)
+syntax (xsymbols)
"op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
@@ -638,7 +635,7 @@
"_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
-syntax (symbols)
+syntax (xsymbols)
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
--- a/src/HOL/Hyperreal/NSA.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Fri Nov 09 00:09:47 2001 +0100
@@ -38,7 +38,7 @@
(*standard real numbers as a subset of the hyperreals*)
SReal_def "Reals == {x. EX r. x = hypreal_of_real r}"
-syntax (symbols)
+syntax (xsymbols)
approx :: "[hypreal, hypreal] => bool" (infixl "\\<approx>" 50)
end
--- a/src/HOL/Lambda/Type.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Lambda/Type.thy Fri Nov 09 00:09:47 2001 +0100
@@ -20,7 +20,7 @@
constdefs
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91)
"e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
-syntax (symbols)
+syntax (xsymbols)
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
@@ -56,7 +56,7 @@
"_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50)
"_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
("_ ||- _ : _" [50, 50, 50] 50)
-syntax (symbols)
+syntax (xsymbols)
"_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
syntax (latex)
"_funs" :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "\<Rrightarrow>" 200)
--- a/src/HOL/Lattice/CompleteLattice.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Fri Nov 09 00:09:47 2001 +0100
@@ -34,7 +34,7 @@
consts
Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
Join :: "'a::complete_lattice set \<Rightarrow> 'a"
-syntax (symbols)
+syntax (xsymbols)
Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
defs
--- a/src/HOL/Lattice/Lattice.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Lattice/Lattice.thy Fri Nov 09 00:09:47 2001 +0100
@@ -27,7 +27,7 @@
consts
meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70)
join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65)
-syntax (symbols)
+syntax (xsymbols)
meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
defs
--- a/src/HOL/Lattice/Orders.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Lattice/Orders.thy Fri Nov 09 00:09:47 2001 +0100
@@ -21,7 +21,7 @@
axclass leq < "term"
consts
leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
-syntax (symbols)
+syntax (xsymbols)
leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
axclass quasi_order < leq
--- a/src/HOL/List.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/List.thy Fri Nov 09 00:09:47 2001 +0100
@@ -64,7 +64,7 @@
"[i..j]" == "[i..(Suc j)(]"
-syntax (symbols)
+syntax (xsymbols)
"@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
--- a/src/HOL/Map.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Map.thy Fri Nov 09 00:09:47 2001 +0100
@@ -23,7 +23,7 @@
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
("_/'(_/|->_')" [900,0,0]900)
-syntax (symbols)
+syntax (xsymbols)
"~=>" :: [type, type] => type (infixr "\\<leadsto>" 0)
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
("_/'(_/\\<mapsto>/_')" [900,0,0]900)
--- a/src/HOL/Product_Type.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Product_Type.thy Fri Nov 09 00:09:47 2001 +0100
@@ -77,7 +77,7 @@
by blast
qed
-syntax (symbols)
+syntax (xsymbols)
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
syntax (HTML output)
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
@@ -129,7 +129,7 @@
"SIGMA x:A. B" => "Sigma A (%x. B)"
"A <*> B" => "Sigma A (_K B)"
-syntax (symbols)
+syntax (xsymbols)
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Nov 09 00:09:47 2001 +0100
@@ -18,7 +18,7 @@
consts
prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
-syntax (symbols)
+syntax (xsymbols)
prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
--- a/src/HOL/Real/RealDef.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Real/RealDef.thy Fri Nov 09 00:09:47 2001 +0100
@@ -86,7 +86,7 @@
real_le_def
"P <= (Q::real) == ~(Q < P)"
-syntax (symbols)
+syntax (xsymbols)
Reals :: "'a set" ("\\<real>")
Nats :: "'a set" ("\\<nat>")
--- a/src/HOL/Set.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Set.thy Fri Nov 09 00:09:47 2001 +0100
@@ -91,7 +91,7 @@
"_setless" :: "'a set => 'a set => bool" ("op <")
"_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50)
-syntax (symbols)
+syntax (xsymbols)
"_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")
"_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50)
"_setless" :: "'a set => 'a set => bool" ("op \<subset>")
--- a/src/HOL/TLA/Intensional.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/TLA/Intensional.thy Fri Nov 09 00:09:47 2001 +0100
@@ -146,14 +146,14 @@
"w |= EX x. A" <= "_REx x A w"
"w |= EX! x. A" <= "_REx1 x A w"
-syntax (symbols)
+syntax (xsymbols)
"_Valid" :: lift => bool ("(\\<turnstile> _)" 5)
"_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10)
"_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50)
"_liftNot" :: lift => lift ("\\<not> _" [40] 40)
"_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35)
"_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30)
- "_liftImp" :: [lift, lift] => lift (infixr "\\<midarrow>\\<rightarrow>" 25)
+ "_liftImp" :: [lift, lift] => lift (infixr "\\<longrightarrow>" 25)
"_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10)
"_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10)
"_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10)
--- a/src/HOL/TLA/TLA.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/TLA/TLA.thy Fri Nov 09 00:09:47 2001 +0100
@@ -55,7 +55,7 @@
"sigma |= EEX x. F" <= "_EEx x F sigma"
"sigma |= AALL x. F" <= "_AAll x F sigma"
-syntax (symbols)
+syntax (xsymbols)
"_Box" :: lift => lift ("(\\<box>_)" [40] 40)
"_Dmd" :: lift => lift ("(\\<diamond>_)" [40] 40)
"_leadsto" :: [lift,lift] => lift ("(_ \\<leadsto> _)" [23,22] 22)
--- a/src/HOL/UNITY/Union.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/UNITY/Union.thy Fri Nov 09 00:09:47 2001 +0100
@@ -45,7 +45,7 @@
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "JOIN UNIV (%x. B)"
-syntax (symbols)
+syntax (xsymbols)
SKIP :: 'a program ("\\<bottom>")
"op Join" :: ['a program, 'a program] => 'a program (infixl "\\<squnion>" 65)
"@JOIN1" :: [pttrns, 'b set] => 'b set ("(3\\<Squnion> _./ _)" 10)
--- a/src/HOL/ex/Tuple.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/ex/Tuple.thy Fri Nov 09 00:09:47 2001 +0100
@@ -38,7 +38,7 @@
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ */ _" [21, 20] 20)
"_tuple_type" :: "type => tuple_type_args => type" ("(_ */ _)" [21, 20] 20)
-syntax (symbols)
+syntax (xsymbols)
"_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
"_tuple_type" :: "type => tuple_type_args => type" ("(_ \<times>/ _)" [21, 20] 20)
--- a/src/HOLCF/Cfun1.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Cfun1.thy Fri Nov 09 00:09:47 2001 +0100
@@ -23,7 +23,7 @@
(* abstraction *)
less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
-syntax (symbols)
+syntax (xsymbols)
"->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [1,0]0)
"LAM " :: "[idts, 'a => 'b] => ('a -> 'b)"
("(3\\<Lambda>_./ _)" [0, 10] 10)
--- a/src/HOLCF/Cprod3.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Cprod3.thy Fri Nov 09 00:09:47 2001 +0100
@@ -72,7 +72,7 @@
"LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)"
"LAM <x,y>.b" == "csplit$(LAM x y. b)"
-syntax (symbols)
+syntax (xsymbols)
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
end
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Fri Nov 09 00:09:47 2001 +0100
@@ -83,10 +83,10 @@
"local" :: "('a,'s)ioa => 'a set"
-syntax (symbols)
+syntax (xsymbols)
"_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool"
- ("_ \\<midarrow>_\\<midarrow>_\\<midarrow>\\<rightarrow> _" [81,81,81,81] 100)
+ ("_ \\<midarrow>_\\<midarrow>_\\<longrightarrow> _" [81,81,81,81] 100)
"op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\\<parallel>" 10)
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Fri Nov 09 00:09:47 2001 +0100
@@ -32,13 +32,13 @@
"OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "|" 30)
"IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25)
-syntax (symbols output)
+syntax (xsymbols output)
"NOT" ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
"AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<and>" 35)
"OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<or>" 30)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<midarrow>\\<rightarrow>" 25)
+ "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<longrightarrow>" 25)
-syntax (symbols)
+syntax (xsymbols)
"satisfies" ::"'a => 'a predicate => bool" ("_ \\<Turnstile> _" [100,9] 8)
syntax (HTML output)
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Fri Nov 09 00:09:47 2001 +0100
@@ -35,7 +35,7 @@
"_partlist" :: args => 'a Seq ("[(_)?]")
-syntax (symbols)
+syntax (xsymbols)
"@Consq" ::"'a => 'a Seq => 'a Seq" ("(_\\<leadsto>_)" [66,65] 65)
--- a/src/HOLCF/IOA/meta_theory/TL.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Fri Nov 09 00:09:47 2001 +0100
@@ -35,7 +35,7 @@
Next ::"'a temporal => 'a temporal"
Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22)
-syntax (symbols)
+syntax (xsymbols)
"Box" ::"'a temporal => 'a temporal" ("\\<box> (_)" [80] 80)
"Diamond" ::"'a temporal => 'a temporal" ("\\<diamond> (_)" [80] 80)
"Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\\<leadsto>" 22)
--- a/src/HOLCF/Pcpo.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Pcpo.thy Fri Nov 09 00:09:47 2001 +0100
@@ -22,7 +22,7 @@
consts
UU :: "'a::pcpo"
-syntax (symbols)
+syntax (xsymbols)
UU :: "'a::pcpo" ("\\<bottom>")
defs
--- a/src/HOLCF/Porder.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Porder.thy Fri Nov 09 00:09:47 2001 +0100
@@ -25,7 +25,7 @@
"LUB x. t" == "lub(range(%x. t))"
-syntax (symbols)
+syntax (xsymbols)
"LUB " :: "[idts, 'a] => 'a" ("(3\\<Squnion>_./ _)"[0,10] 10)
--- a/src/HOLCF/Porder0.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Porder0.thy Fri Nov 09 00:09:47 2001 +0100
@@ -15,7 +15,7 @@
consts
"<<" :: "['a,'a::sq_ord] => bool" (infixl 55)
-syntax (symbols)
+syntax (xsymbols)
"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\<sqsubseteq>" 55)
axclass po < sq_ord
--- a/src/HOLCF/Sprod0.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Sprod0.thy Fri Nov 09 00:09:47 2001 +0100
@@ -14,7 +14,7 @@
typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
-syntax (symbols)
+syntax (xsymbols)
"**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
consts
--- a/src/HOLCF/Ssum0.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOLCF/Ssum0.thy Fri Nov 09 00:09:47 2001 +0100
@@ -17,7 +17,7 @@
typedef (Ssum) ('a, 'b) "++" (infixr 10) =
"{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}"
-syntax (symbols)
+syntax (xsymbols)
"++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
consts
--- a/src/ZF/Arith.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/Arith.thy Fri Nov 09 00:09:47 2001 +0100
@@ -56,7 +56,7 @@
mod :: [i,i]=>i (infixl "mod" 70)
"m mod n == raw_mod (natify(m), natify(n))"
-syntax (symbols)
+syntax (xsymbols)
"mult" :: [i, i] => i (infixr "#\\<times>" 70)
syntax (HTML output)
--- a/src/ZF/CardinalArith.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/CardinalArith.thy Fri Nov 09 00:09:47 2001 +0100
@@ -39,7 +39,7 @@
(*needed because jump_cardinal(K) might not be the successor of K*)
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
-syntax (symbols)
+syntax (xsymbols)
"op |+|" :: [i,i] => i (infixl "\\<oplus>" 65)
"op |*|" :: [i,i] => i (infixl "\\<otimes>" 70)
--- a/src/ZF/Integ/Int.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/Integ/Int.thy Fri Nov 09 00:09:47 2001 +0100
@@ -76,7 +76,7 @@
"z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
-syntax (symbols)
+syntax (xsymbols)
"zmult" :: [i,i] => i (infixl "$\\<times>" 70)
"zle" :: [i,i] => o (infixl "$\\<le>" 50) (*less than / equals*)
--- a/src/ZF/OrdQuant.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/OrdQuant.thy Fri Nov 09 00:09:47 2001 +0100
@@ -25,7 +25,7 @@
"EX x<a. P" == "oex(a, %x. P)"
"UN x<a. B" == "OUnion(a, %x. B)"
-syntax (symbols)
+syntax (xsymbols)
"@oall" :: [idt, i, o] => o ("(3\\<forall> _<_./ _)" 10)
"@oex" :: [idt, i, o] => o ("(3\\<exists> _<_./ _)" 10)
"@OUNION" :: [idt, i, i] => i ("(3\\<Union> _<_./ _)" 10)
--- a/src/ZF/OrderType.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/OrderType.thy Fri Nov 09 00:09:47 2001 +0100
@@ -38,7 +38,7 @@
(*ordinal subtraction*)
odiff_def "i -- j == ordertype(i-j, Memrel(i))"
-syntax (symbols)
+syntax (xsymbols)
"op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
syntax (HTML output)
--- a/src/ZF/Ordinal.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/Ordinal.thy Fri Nov 09 00:09:47 2001 +0100
@@ -19,7 +19,7 @@
translations
"x le y" == "x < succ(y)"
-syntax (symbols)
+syntax (xsymbols)
"op le" :: [i,i] => o (infixl "\\<le>" 50) (*less than or equals*)
defs
--- a/src/ZF/UNITY/Union.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/UNITY/Union.thy Fri Nov 09 00:09:47 2001 +0100
@@ -50,7 +50,7 @@
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "JOIN(state,(%x. B))"
-syntax (symbols)
+syntax (xsymbols)
SKIP :: i ("\\<bottom>")
"op Join" :: [i, i] => i (infixl "\\<squnion>" 65)
"@JOIN1" :: [pttrns, i] => i ("(3\\<Squnion> _./ _)" 10)
--- a/src/ZF/ZF.thy Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/ZF.thy Fri Nov 09 00:09:47 2001 +0100
@@ -142,7 +142,7 @@
"%<x,y>.b" == "split(%x y. b)"
-syntax (symbols)
+syntax (xsymbols)
"op *" :: [i, i] => i (infixr "\\<times>" 80)
"op Int" :: [i, i] => i (infixl "\\<inter>" 70)
"op Un" :: [i, i] => i (infixl "\\<union>" 65)
@@ -160,8 +160,6 @@
"@lam" :: [pttrn, i, i] => i ("(3\\<lambda>_\\<in>_./ _)" 10)
"@Ball" :: [pttrn, i, o] => o ("(3\\<forall>_\\<in>_./ _)" 10)
"@Bex" :: [pttrn, i, o] => o ("(3\\<exists>_\\<in>_./ _)" 10)
-
-syntax (xsymbols)
"@Tuple" :: [i, is] => i ("\\<langle>(_,/ _)\\<rangle>")
"@pattern" :: patterns => pttrn ("\\<langle>_\\<rangle>")