--- 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)
--- 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
--- 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)