# HG changeset patch
# User wenzelm
# Date 1005260453 -3600
# Node ID f8b4b11cd79d75d07be3ae58aaf5086e9b22bb44
# Parent  bd6eb9194a5d95cfc202d0f3b081a82d5b87f52a
eliminated old "symbols" syntax, use "xsymbols" instead;

diff -r bd6eb9194a5d -r f8b4b11cd79d src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Thu Nov 08 23:59:37 2001 +0100
+++ b/src/CTT/Arith.thy	Fri Nov 09 00:00:53 2001 +0100
@@ -14,7 +14,7 @@
 consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
        "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
 
-syntax (symbols)
+syntax (xsymbols)
   "op #*"      :: [i, i] => i   (infixr "#\\<times>" 70)
 
 syntax (HTML output)
diff -r bd6eb9194a5d -r f8b4b11cd79d src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Thu Nov 08 23:59:37 2001 +0100
+++ b/src/CTT/CTT.thy	Fri Nov 09 00:00:53 2001 +0100
@@ -67,13 +67,11 @@
 syntax (xsymbols)
   "@-->"    :: "[t,t]=>t"           ("(_ \\<longrightarrow>/ _)" [31,30] 30)
   "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
-
-syntax (symbols)
-  Elem      :: "[i, t]=>prop"     ("(_ /\\<in> _)" [10,10] 5)
-  Eqelem    :: "[i,i,t]=>prop"    ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
-  "@SUM"    :: "[idt,t,t] => t"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
-  "@PROD"   :: "[idt,t,t] => t"   ("(3\\<Pi> _\\<in>_./ _)"    10)
-  "lam "    :: "[idts, i] => i"   ("(3\\<lambda>\\<lambda>_./ _)" 10)
+  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
+  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
+  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
+  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
 
 rules
 
diff -r bd6eb9194a5d -r f8b4b11cd79d src/Cube/Base.thy
--- a/src/Cube/Base.thy	Thu Nov 08 23:59:37 2001 +0100
+++ b/src/Cube/Base.thy	Fri Nov 09 00:00:53 2001 +0100
@@ -38,7 +38,7 @@
   "Pi x:A. B"   => "Prod(A, %x. B)"
   "A -> B"      => "Prod(A, _K(B))"
 
-syntax (symbols)
+syntax (xsymbols)
   Trueprop      :: "[context, typing] => prop"          ("(_/ \\<turnstile> _)")
   box           :: "term"                               ("\\<box>")
   Lam           :: "[idt, term, term] => term"          ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10)