# HG changeset patch
# User wenzelm
# Date 1005260987 -3600
# Node ID a8e860c862525a10c82dab08e4033b29cd9cf2fb
# Parent  46a14ebdac4fc606b46c74fead0d3bf528b6f672
eliminated old "symbols" syntax, use "xsymbols" instead;

diff -r 46a14ebdac4f -r a8e860c86252 src/FOL/IFOL.thy
--- 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)
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Finite.thy
--- 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! *)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Fun.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/GroupTheory/Group.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/HOL.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Hyperreal/NSA.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Lambda/Type.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Lattice/CompleteLattice.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Lattice/Lattice.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Lattice/Orders.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/List.thy
--- 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>_ ./ _])")
 
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Map.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Product_Type.thy
--- 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)
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Real/HahnBanach/VectorSpace.thy
--- 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)
 
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Real/RealDef.thy
--- 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>")
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Set.thy
--- 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>")
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/TLA/Intensional.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/TLA/TLA.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/UNITY/Union.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/ex/Tuple.thy
--- 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)
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Cfun1.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Cprod3.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/IOA/meta_theory/Automata.thy
--- 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)
 
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/IOA/meta_theory/Pred.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/IOA/meta_theory/Sequence.thy
--- 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)
  
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/IOA/meta_theory/TL.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Pcpo.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Porder.thy
--- 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)
 
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Porder0.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Sprod0.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/HOLCF/Ssum0.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/Arith.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/CardinalArith.thy
--- 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)
 
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/Integ/Int.thy
--- 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*)
 
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/OrdQuant.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/OrderType.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/Ordinal.thy
--- 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
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/UNITY/Union.thy
--- 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)
diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/ZF.thy
--- 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>")