eliminated old "symbols" syntax, use "xsymbols" instead;
authorwenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114a8e860c86252
parent 12113 46a14ebdac4f
child 12115 d0d41884f787
eliminated old "symbols" syntax, use "xsymbols" instead;
src/FOL/IFOL.thy
src/HOL/Finite.thy
src/HOL/Fun.thy
src/HOL/GroupTheory/Group.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Lambda/Type.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Product_Type.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/TLA.thy
src/HOL/UNITY/Union.thy
src/HOL/ex/Tuple.thy
src/HOLCF/Cfun1.thy
src/HOLCF/Cprod3.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Porder0.thy
src/HOLCF/Sprod0.thy
src/HOLCF/Ssum0.thy
src/ZF/Arith.thy
src/ZF/CardinalArith.thy
src/ZF/Integ/Int.thy
src/ZF/OrdQuant.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/UNITY/Union.thy
src/ZF/ZF.thy
     1.1 --- a/src/FOL/IFOL.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -47,18 +47,14 @@
     1.4  translations
     1.5    "x ~= y"      == "~ (x = y)"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    Not           :: "o => o"                     ("\<not> _" [40] 40)
    1.10    "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    1.11    "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    1.12 -  "op -->"      :: "[o, o] => o"                (infixr "\<midarrow>\<rightarrow>" 25)
    1.13 -  "op <->"      :: "[o, o] => o"                (infixr "\<leftarrow>\<rightarrow>" 25)
    1.14    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.15    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.16    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.17    "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.18 -
    1.19 -syntax (xsymbols)
    1.20    "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    1.21    "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    1.22  
     2.1 --- a/src/HOL/Finite.thy	Fri Nov 09 00:06:15 2001 +0100
     2.2 +++ b/src/HOL/Finite.thy	Fri Nov 09 00:09:47 2001 +0100
     2.3 @@ -63,7 +63,7 @@
     2.4  
     2.5  syntax
     2.6    "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_:_. _" [0, 51, 10] 10)
     2.7 -syntax (symbols)
     2.8 +syntax (xsymbols)
     2.9    "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10)
    2.10  translations
    2.11    "\\<Sum>i:A. b" == "setsum (%i. b) A"  (* Beware of argument permutation! *)
     3.1 --- a/src/HOL/Fun.thy	Fri Nov 09 00:06:15 2001 +0100
     3.2 +++ b/src/HOL/Fun.thy	Fri Nov 09 00:09:47 2001 +0100
     3.3 @@ -46,7 +46,7 @@
     3.4    inj_on :: ['a => 'b, 'a set] => bool
     3.5      "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     3.6  
     3.7 -syntax (symbols)
     3.8 +syntax (xsymbols)
     3.9    "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
    3.10  
    3.11  syntax
    3.12 @@ -79,7 +79,7 @@
    3.13  
    3.14    (*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
    3.15  
    3.16 -syntax (symbols)
    3.17 +syntax (xsymbols)
    3.18    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
    3.19  
    3.20  translations
     4.1 --- a/src/HOL/GroupTheory/Group.thy	Fri Nov 09 00:06:15 2001 +0100
     4.2 +++ b/src/HOL/GroupTheory/Group.thy	Fri Nov 09 00:09:47 2001 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  Group = Main +
     4.5  
     4.6    (*Giving funcset the nice arrow syntax \\<rightarrow> *)
     4.7 -syntax (symbols)
     4.8 +syntax (xsymbols)
     4.9    "op funcset" :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\\<rightarrow>" 60) 
    4.10  
    4.11  
    4.12 @@ -21,7 +21,7 @@
    4.13  record 'a grouptype = 'a semigrouptype +
    4.14    inverse  :: "'a => 'a"
    4.15    unit     :: "'a"
    4.16 -(* This should be obsolete, if records will allow the promised syntax *)
    4.17 +
    4.18  syntax 
    4.19    "@carrier" :: "'a semigrouptype => 'a set"            ("_ .<cr>"  [10] 10)
    4.20    "@bin_op"  :: "'a semigrouptype => (['a, 'a] => 'a)"  ("_ .<f>"   [10] 10)
     5.1 --- a/src/HOL/HOL.thy	Fri Nov 09 00:06:15 2001 +0100
     5.2 +++ b/src/HOL/HOL.thy	Fri Nov 09 00:09:47 2001 +0100
     5.3 @@ -78,11 +78,11 @@
     5.4    "="           :: "['a, 'a] => bool"                    (infix 50)
     5.5    "~="          :: "['a, 'a] => bool"                    (infix 50)
     5.6  
     5.7 -syntax (symbols)
     5.8 +syntax (xsymbols)
     5.9    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    5.10    "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    5.11    "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    5.12 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<midarrow>\<rightarrow>" 25)
    5.13 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    5.14    "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    5.15    "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    5.16    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    5.17 @@ -90,12 +90,9 @@
    5.18    "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    5.19  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    5.20  
    5.21 -syntax (symbols output)
    5.22 +syntax (xsymbols output)
    5.23    "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    5.24  
    5.25 -syntax (xsymbols)
    5.26 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    5.27 -
    5.28  syntax (HTML output)
    5.29    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    5.30  
    5.31 @@ -353,7 +350,7 @@
    5.32  
    5.33  local
    5.34  
    5.35 -syntax (symbols)
    5.36 +syntax (xsymbols)
    5.37    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    5.38    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    5.39  
    5.40 @@ -638,7 +635,7 @@
    5.41    "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
    5.42    "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
    5.43  
    5.44 -syntax (symbols)
    5.45 +syntax (xsymbols)
    5.46    "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
    5.47    "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
    5.48    "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
     6.1 --- a/src/HOL/Hyperreal/NSA.thy	Fri Nov 09 00:06:15 2001 +0100
     6.2 +++ b/src/HOL/Hyperreal/NSA.thy	Fri Nov 09 00:09:47 2001 +0100
     6.3 @@ -38,7 +38,7 @@
     6.4     (*standard real numbers as a subset of the hyperreals*)
     6.5     SReal_def      "Reals == {x. EX r. x = hypreal_of_real r}"
     6.6  
     6.7 -syntax (symbols)
     6.8 +syntax (xsymbols)
     6.9      approx :: "[hypreal, hypreal] => bool"    (infixl "\\<approx>" 50)
    6.10    
    6.11  end
     7.1 --- a/src/HOL/Lambda/Type.thy	Fri Nov 09 00:06:15 2001 +0100
     7.2 +++ b/src/HOL/Lambda/Type.thy	Fri Nov 09 00:09:47 2001 +0100
     7.3 @@ -20,7 +20,7 @@
     7.4  constdefs
     7.5    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
     7.6    "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
     7.7 -syntax (symbols)
     7.8 +syntax (xsymbols)
     7.9    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    7.10  
    7.11  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    7.12 @@ -56,7 +56,7 @@
    7.13    "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
    7.14    "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    7.15      ("_ ||- _ : _" [50, 50, 50] 50)
    7.16 -syntax (symbols)
    7.17 +syntax (xsymbols)
    7.18    "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    7.19  syntax (latex)
    7.20    "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
     8.1 --- a/src/HOL/Lattice/CompleteLattice.thy	Fri Nov 09 00:06:15 2001 +0100
     8.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Fri Nov 09 00:09:47 2001 +0100
     8.3 @@ -34,7 +34,7 @@
     8.4  consts
     8.5    Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
     8.6    Join :: "'a::complete_lattice set \<Rightarrow> 'a"
     8.7 -syntax (symbols)
     8.8 +syntax (xsymbols)
     8.9    Meet :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Sqinter>_" [90] 90)
    8.10    Join :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
    8.11  defs
     9.1 --- a/src/HOL/Lattice/Lattice.thy	Fri Nov 09 00:06:15 2001 +0100
     9.2 +++ b/src/HOL/Lattice/Lattice.thy	Fri Nov 09 00:09:47 2001 +0100
     9.3 @@ -27,7 +27,7 @@
     9.4  consts
     9.5    meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70)
     9.6    join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65)
     9.7 -syntax (symbols)
     9.8 +syntax (xsymbols)
     9.9    meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70)
    9.10    join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65)
    9.11  defs
    10.1 --- a/src/HOL/Lattice/Orders.thy	Fri Nov 09 00:06:15 2001 +0100
    10.2 +++ b/src/HOL/Lattice/Orders.thy	Fri Nov 09 00:09:47 2001 +0100
    10.3 @@ -21,7 +21,7 @@
    10.4  axclass leq < "term"
    10.5  consts
    10.6    leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
    10.7 -syntax (symbols)
    10.8 +syntax (xsymbols)
    10.9    leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sqsubseteq>" 50)
   10.10  
   10.11  axclass quasi_order < leq
    11.1 --- a/src/HOL/List.thy	Fri Nov 09 00:06:15 2001 +0100
    11.2 +++ b/src/HOL/List.thy	Fri Nov 09 00:09:47 2001 +0100
    11.3 @@ -64,7 +64,7 @@
    11.4    "[i..j]" == "[i..(Suc j)(]"
    11.5  
    11.6  
    11.7 -syntax (symbols)
    11.8 +syntax (xsymbols)
    11.9    "@filter"   :: [pttrn, 'a list, bool] => 'a list        ("(1[_\\<in>_ ./ _])")
   11.10  
   11.11  
    12.1 --- a/src/HOL/Map.thy	Fri Nov 09 00:06:15 2001 +0100
    12.2 +++ b/src/HOL/Map.thy	Fri Nov 09 00:09:47 2001 +0100
    12.3 @@ -23,7 +23,7 @@
    12.4  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    12.5  					         ("_/'(_/|->_')"   [900,0,0]900)
    12.6  
    12.7 -syntax (symbols)
    12.8 +syntax (xsymbols)
    12.9    "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
   12.10    map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
   12.11  					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
    13.1 --- a/src/HOL/Product_Type.thy	Fri Nov 09 00:06:15 2001 +0100
    13.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 09 00:09:47 2001 +0100
    13.3 @@ -77,7 +77,7 @@
    13.4      by blast
    13.5  qed
    13.6  
    13.7 -syntax (symbols)
    13.8 +syntax (xsymbols)
    13.9    "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
   13.10  syntax (HTML output)
   13.11    "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
   13.12 @@ -129,7 +129,7 @@
   13.13    "SIGMA x:A. B" => "Sigma A (%x. B)"
   13.14    "A <*> B"      => "Sigma A (_K B)"
   13.15  
   13.16 -syntax (symbols)
   13.17 +syntax (xsymbols)
   13.18    "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   13.19    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   13.20  
    14.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Nov 09 00:06:15 2001 +0100
    14.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Nov 09 00:09:47 2001 +0100
    14.3 @@ -18,7 +18,7 @@
    14.4  consts
    14.5    prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)
    14.6  
    14.7 -syntax (symbols)
    14.8 +syntax (xsymbols)
    14.9    prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
   14.10  
   14.11  
    15.1 --- a/src/HOL/Real/RealDef.thy	Fri Nov 09 00:06:15 2001 +0100
    15.2 +++ b/src/HOL/Real/RealDef.thy	Fri Nov 09 00:09:47 2001 +0100
    15.3 @@ -86,7 +86,7 @@
    15.4    real_le_def
    15.5    "P <= (Q::real) == ~(Q < P)"
    15.6  
    15.7 -syntax (symbols)
    15.8 +syntax (xsymbols)
    15.9    Reals     :: "'a set"                   ("\\<real>")
   15.10    Nats      :: "'a set"                   ("\\<nat>")
   15.11  
    16.1 --- a/src/HOL/Set.thy	Fri Nov 09 00:06:15 2001 +0100
    16.2 +++ b/src/HOL/Set.thy	Fri Nov 09 00:09:47 2001 +0100
    16.3 @@ -91,7 +91,7 @@
    16.4    "_setless"    :: "'a set => 'a set => bool"             ("op <")
    16.5    "_setless"    :: "'a set => 'a set => bool"             ("(_/ < _)" [50, 51] 50)
    16.6  
    16.7 -syntax (symbols)
    16.8 +syntax (xsymbols)
    16.9    "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
   16.10    "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
   16.11    "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
    17.1 --- a/src/HOL/TLA/Intensional.thy	Fri Nov 09 00:06:15 2001 +0100
    17.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Nov 09 00:09:47 2001 +0100
    17.3 @@ -146,14 +146,14 @@
    17.4    "w |= EX x. A"   <= "_REx x A w"
    17.5    "w |= EX! x. A"  <= "_REx1 x A w"
    17.6  
    17.7 -syntax (symbols)
    17.8 +syntax (xsymbols)
    17.9    "_Valid"      :: lift => bool                        ("(\\<turnstile> _)" 5)
   17.10    "_holdsAt"    :: ['a, lift] => bool                  ("(_ \\<Turnstile> _)" [100,10] 10)
   17.11    "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
   17.12    "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
   17.13    "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
   17.14    "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
   17.15 -  "_liftImp"    :: [lift, lift] => lift                (infixr "\\<midarrow>\\<rightarrow>" 25)
   17.16 +  "_liftImp"    :: [lift, lift] => lift                (infixr "\\<longrightarrow>" 25)
   17.17    "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
   17.18    "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
   17.19    "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
    18.1 --- a/src/HOL/TLA/TLA.thy	Fri Nov 09 00:06:15 2001 +0100
    18.2 +++ b/src/HOL/TLA/TLA.thy	Fri Nov 09 00:09:47 2001 +0100
    18.3 @@ -55,7 +55,7 @@
    18.4    "sigma |= EEX x. F"    <= "_EEx x F sigma"
    18.5    "sigma |= AALL x. F"    <= "_AAll x F sigma"
    18.6  
    18.7 -syntax (symbols)
    18.8 +syntax (xsymbols)
    18.9    "_Box"     :: lift => lift                        ("(\\<box>_)" [40] 40)
   18.10    "_Dmd"     :: lift => lift                        ("(\\<diamond>_)" [40] 40)
   18.11    "_leadsto" :: [lift,lift] => lift                 ("(_ \\<leadsto> _)" [23,22] 22)
    19.1 --- a/src/HOL/UNITY/Union.thy	Fri Nov 09 00:06:15 2001 +0100
    19.2 +++ b/src/HOL/UNITY/Union.thy	Fri Nov 09 00:09:47 2001 +0100
    19.3 @@ -45,7 +45,7 @@
    19.4    "JN x y. B"   == "JN x. JN y. B"
    19.5    "JN x. B"     == "JOIN UNIV (%x. B)"
    19.6  
    19.7 -syntax (symbols)
    19.8 +syntax (xsymbols)
    19.9    SKIP      :: 'a program                              ("\\<bottom>")
   19.10    "op Join" :: ['a program, 'a program] => 'a program  (infixl "\\<squnion>" 65)
   19.11    "@JOIN1"  :: [pttrns, 'b set] => 'b set              ("(3\\<Squnion> _./ _)" 10)
    20.1 --- a/src/HOL/ex/Tuple.thy	Fri Nov 09 00:06:15 2001 +0100
    20.2 +++ b/src/HOL/ex/Tuple.thy	Fri Nov 09 00:09:47 2001 +0100
    20.3 @@ -38,7 +38,7 @@
    20.4    "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ */ _" [21, 20] 20)
    20.5    "_tuple_type"      :: "type => tuple_type_args => type"            ("(_ */ _)" [21, 20] 20)
    20.6  
    20.7 -syntax (symbols)
    20.8 +syntax (xsymbols)
    20.9    "_tuple_type_args" :: "type => tuple_type_args => tuple_type_args" ("_ \<times>/ _" [21, 20] 20)
   20.10    "_tuple_type"      :: "type => tuple_type_args => type"          ("(_ \<times>/ _)" [21, 20] 20)
   20.11  
    21.1 --- a/src/HOLCF/Cfun1.thy	Fri Nov 09 00:06:15 2001 +0100
    21.2 +++ b/src/HOLCF/Cfun1.thy	Fri Nov 09 00:09:47 2001 +0100
    21.3 @@ -23,7 +23,7 @@
    21.4                                                  (* abstraction      *)
    21.5          less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    21.6  
    21.7 -syntax (symbols)
    21.8 +syntax (xsymbols)
    21.9    "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
   21.10    "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
   21.11  					("(3\\<Lambda>_./ _)" [0, 10] 10)
    22.1 --- a/src/HOLCF/Cprod3.thy	Fri Nov 09 00:06:15 2001 +0100
    22.2 +++ b/src/HOLCF/Cprod3.thy	Fri Nov 09 00:09:47 2001 +0100
    22.3 @@ -72,7 +72,7 @@
    22.4    "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
    22.5    "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
    22.6  
    22.7 -syntax (symbols)
    22.8 +syntax (xsymbols)
    22.9    "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
   22.10  
   22.11  end
    23.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Fri Nov 09 00:06:15 2001 +0100
    23.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Fri Nov 09 00:09:47 2001 +0100
    23.3 @@ -83,10 +83,10 @@
    23.4    "local"      :: "('a,'s)ioa => 'a set"
    23.5  
    23.6  
    23.7 -syntax (symbols)
    23.8 +syntax (xsymbols)
    23.9  
   23.10    "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"  
   23.11 -                  ("_ \\<midarrow>_\\<midarrow>_\\<midarrow>\\<rightarrow> _" [81,81,81,81] 100)
   23.12 +                  ("_ \\<midarrow>_\\<midarrow>_\\<longrightarrow> _" [81,81,81,81] 100)
   23.13    "op ||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "\\<parallel>" 10)
   23.14  
   23.15  
    24.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Fri Nov 09 00:06:15 2001 +0100
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Fri Nov 09 00:09:47 2001 +0100
    24.3 @@ -32,13 +32,13 @@
    24.4    "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)
    24.5    "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)
    24.6  
    24.7 -syntax (symbols output)
    24.8 +syntax (xsymbols output)
    24.9    "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
   24.10    "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
   24.11    "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
   24.12 -  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<midarrow>\\<rightarrow>" 25)
   24.13 +  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<longrightarrow>" 25)
   24.14  
   24.15 -syntax (symbols)
   24.16 +syntax (xsymbols)
   24.17    "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
   24.18  
   24.19  syntax (HTML output)
    25.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Nov 09 00:06:15 2001 +0100
    25.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Nov 09 00:09:47 2001 +0100
    25.3 @@ -35,7 +35,7 @@
    25.4    "_partlist"     :: args => 'a Seq                          ("[(_)?]")
    25.5  
    25.6  
    25.7 -syntax (symbols)
    25.8 +syntax (xsymbols)
    25.9  
   25.10   "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
   25.11   
    26.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Fri Nov 09 00:06:15 2001 +0100
    26.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Fri Nov 09 00:09:47 2001 +0100
    26.3 @@ -35,7 +35,7 @@
    26.4  Next         ::"'a temporal => 'a temporal"   
    26.5  Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
    26.6  
    26.7 -syntax (symbols)
    26.8 +syntax (xsymbols)
    26.9     "Box"        ::"'a temporal => 'a temporal"   ("\\<box> (_)" [80] 80)
   26.10     "Diamond"    ::"'a temporal => 'a temporal"   ("\\<diamond> (_)" [80] 80)
   26.11     "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\\<leadsto>" 22)
    27.1 --- a/src/HOLCF/Pcpo.thy	Fri Nov 09 00:06:15 2001 +0100
    27.2 +++ b/src/HOLCF/Pcpo.thy	Fri Nov 09 00:09:47 2001 +0100
    27.3 @@ -22,7 +22,7 @@
    27.4  consts
    27.5    UU            :: "'a::pcpo"        
    27.6  
    27.7 -syntax (symbols)
    27.8 +syntax (xsymbols)
    27.9    UU            :: "'a::pcpo"                           ("\\<bottom>")
   27.10  
   27.11  defs
    28.1 --- a/src/HOLCF/Porder.thy	Fri Nov 09 00:06:15 2001 +0100
    28.2 +++ b/src/HOLCF/Porder.thy	Fri Nov 09 00:09:47 2001 +0100
    28.3 @@ -25,7 +25,7 @@
    28.4  
    28.5    "LUB x. t"	== "lub(range(%x. t))"
    28.6  
    28.7 -syntax (symbols)
    28.8 +syntax (xsymbols)
    28.9  
   28.10    "LUB "	:: "[idts, 'a] => 'a"		("(3\\<Squnion>_./ _)"[0,10] 10)
   28.11  
    29.1 --- a/src/HOLCF/Porder0.thy	Fri Nov 09 00:06:15 2001 +0100
    29.2 +++ b/src/HOLCF/Porder0.thy	Fri Nov 09 00:09:47 2001 +0100
    29.3 @@ -15,7 +15,7 @@
    29.4  consts
    29.5    "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
    29.6  
    29.7 -syntax (symbols)
    29.8 +syntax (xsymbols)
    29.9    "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
   29.10  
   29.11  axclass po < sq_ord
    30.1 --- a/src/HOLCF/Sprod0.thy	Fri Nov 09 00:06:15 2001 +0100
    30.2 +++ b/src/HOLCF/Sprod0.thy	Fri Nov 09 00:09:47 2001 +0100
    30.3 @@ -14,7 +14,7 @@
    30.4  
    30.5  typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
    30.6  
    30.7 -syntax (symbols)
    30.8 +syntax (xsymbols)
    30.9    "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
   30.10  
   30.11  consts
    31.1 --- a/src/HOLCF/Ssum0.thy	Fri Nov 09 00:06:15 2001 +0100
    31.2 +++ b/src/HOLCF/Ssum0.thy	Fri Nov 09 00:09:47 2001 +0100
    31.3 @@ -17,7 +17,7 @@
    31.4  typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
    31.5  	"{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}"
    31.6  
    31.7 -syntax (symbols)
    31.8 +syntax (xsymbols)
    31.9    "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
   31.10  
   31.11  consts
    32.1 --- a/src/ZF/Arith.thy	Fri Nov 09 00:06:15 2001 +0100
    32.2 +++ b/src/ZF/Arith.thy	Fri Nov 09 00:09:47 2001 +0100
    32.3 @@ -56,7 +56,7 @@
    32.4    mod  :: [i,i]=>i                    (infixl "mod" 70)
    32.5      "m mod n == raw_mod (natify(m), natify(n))"
    32.6  
    32.7 -syntax (symbols)
    32.8 +syntax (xsymbols)
    32.9    "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
   32.10  
   32.11  syntax (HTML output)
    33.1 --- a/src/ZF/CardinalArith.thy	Fri Nov 09 00:06:15 2001 +0100
    33.2 +++ b/src/ZF/CardinalArith.thy	Fri Nov 09 00:09:47 2001 +0100
    33.3 @@ -39,7 +39,7 @@
    33.4    (*needed because jump_cardinal(K) might not be the successor of K*)
    33.5    csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
    33.6  
    33.7 -syntax (symbols)
    33.8 +syntax (xsymbols)
    33.9    "op |+|"     :: [i,i] => i          (infixl "\\<oplus>" 65)
   33.10    "op |*|"     :: [i,i] => i          (infixl "\\<otimes>" 70)
   33.11  
    34.1 --- a/src/ZF/Integ/Int.thy	Fri Nov 09 00:06:15 2001 +0100
    34.2 +++ b/src/ZF/Integ/Int.thy	Fri Nov 09 00:09:47 2001 +0100
    34.3 @@ -76,7 +76,7 @@
    34.4       "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
    34.5    
    34.6  
    34.7 -syntax (symbols)
    34.8 +syntax (xsymbols)
    34.9    "zmult"     :: [i,i] => i          (infixl "$\\<times>" 70)
   34.10    "zle"       :: [i,i] => o          (infixl "$\\<le>" 50)  (*less than / equals*)
   34.11  
    35.1 --- a/src/ZF/OrdQuant.thy	Fri Nov 09 00:06:15 2001 +0100
    35.2 +++ b/src/ZF/OrdQuant.thy	Fri Nov 09 00:09:47 2001 +0100
    35.3 @@ -25,7 +25,7 @@
    35.4    "EX x<a. P"   == "oex(a, %x. P)"
    35.5    "UN x<a. B"   == "OUnion(a, %x. B)"
    35.6  
    35.7 -syntax (symbols)
    35.8 +syntax (xsymbols)
    35.9    "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
   35.10    "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
   35.11    "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    36.1 --- a/src/ZF/OrderType.thy	Fri Nov 09 00:06:15 2001 +0100
    36.2 +++ b/src/ZF/OrderType.thy	Fri Nov 09 00:09:47 2001 +0100
    36.3 @@ -38,7 +38,7 @@
    36.4    (*ordinal subtraction*)
    36.5    odiff_def     "i -- j == ordertype(i-j, Memrel(i))"
    36.6  
    36.7 -syntax (symbols)
    36.8 +syntax (xsymbols)
    36.9    "op **"     :: [i,i] => i          (infixl "\\<times>\\<times>" 70)
   36.10  
   36.11  syntax (HTML output)
    37.1 --- a/src/ZF/Ordinal.thy	Fri Nov 09 00:06:15 2001 +0100
    37.2 +++ b/src/ZF/Ordinal.thy	Fri Nov 09 00:09:47 2001 +0100
    37.3 @@ -19,7 +19,7 @@
    37.4  translations
    37.5    "x le y"      == "x < succ(y)"
    37.6  
    37.7 -syntax (symbols)
    37.8 +syntax (xsymbols)
    37.9    "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
   37.10  
   37.11  defs
    38.1 --- a/src/ZF/UNITY/Union.thy	Fri Nov 09 00:06:15 2001 +0100
    38.2 +++ b/src/ZF/UNITY/Union.thy	Fri Nov 09 00:09:47 2001 +0100
    38.3 @@ -50,7 +50,7 @@
    38.4    "JN x y. B"   == "JN x. JN y. B"
    38.5    "JN x. B"     == "JOIN(state,(%x. B))"
    38.6  
    38.7 -syntax (symbols)
    38.8 +syntax (xsymbols)
    38.9     SKIP     :: i                    ("\\<bottom>")
   38.10    "op Join" :: [i, i] => i   (infixl "\\<squnion>" 65)
   38.11    "@JOIN1"  :: [pttrns, i] => i     ("(3\\<Squnion> _./ _)" 10)
    39.1 --- a/src/ZF/ZF.thy	Fri Nov 09 00:06:15 2001 +0100
    39.2 +++ b/src/ZF/ZF.thy	Fri Nov 09 00:09:47 2001 +0100
    39.3 @@ -142,7 +142,7 @@
    39.4    "%<x,y>.b"    == "split(%x y. b)"
    39.5  
    39.6  
    39.7 -syntax (symbols)
    39.8 +syntax (xsymbols)
    39.9    "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
   39.10    "op Int"    :: [i, i] => i    	   (infixl "\\<inter>" 70)
   39.11    "op Un"     :: [i, i] => i    	   (infixl "\\<union>" 65)
   39.12 @@ -160,8 +160,6 @@
   39.13    "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda>_\\<in>_./ _)" 10)
   39.14    "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall>_\\<in>_./ _)" 10)
   39.15    "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists>_\\<in>_./ _)" 10)
   39.16 -
   39.17 -syntax (xsymbols)
   39.18    "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
   39.19    "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
   39.20