eliminated old "symbols" syntax, use "xsymbols" instead;
authorwenzelm
Fri Nov 09 00:00:53 2001 +0100 (2001-11-09)
changeset 12110f8b4b11cd79d
parent 12109 bd6eb9194a5d
child 12111 d942348d8faf
eliminated old "symbols" syntax, use "xsymbols" instead;
src/CTT/Arith.thy
src/CTT/CTT.thy
src/Cube/Base.thy
     1.1 --- a/src/CTT/Arith.thy	Thu Nov 08 23:59:37 2001 +0100
     1.2 +++ b/src/CTT/Arith.thy	Fri Nov 09 00:00:53 2001 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
     1.5         "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    "op #*"      :: [i, i] => i   (infixr "#\\<times>" 70)
    1.10  
    1.11  syntax (HTML output)
     2.1 --- a/src/CTT/CTT.thy	Thu Nov 08 23:59:37 2001 +0100
     2.2 +++ b/src/CTT/CTT.thy	Fri Nov 09 00:00:53 2001 +0100
     2.3 @@ -67,13 +67,11 @@
     2.4  syntax (xsymbols)
     2.5    "@-->"    :: "[t,t]=>t"           ("(_ \\<longrightarrow>/ _)" [31,30] 30)
     2.6    "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
     2.7 -
     2.8 -syntax (symbols)
     2.9 -  Elem      :: "[i, t]=>prop"     ("(_ /\\<in> _)" [10,10] 5)
    2.10 -  Eqelem    :: "[i,i,t]=>prop"    ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    2.11 -  "@SUM"    :: "[idt,t,t] => t"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
    2.12 -  "@PROD"   :: "[idt,t,t] => t"   ("(3\\<Pi> _\\<in>_./ _)"    10)
    2.13 -  "lam "    :: "[idts, i] => i"   ("(3\\<lambda>\\<lambda>_./ _)" 10)
    2.14 +  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
    2.15 +  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    2.16 +  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    2.17 +  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
    2.18 +  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
    2.19  
    2.20  rules
    2.21  
     3.1 --- a/src/Cube/Base.thy	Thu Nov 08 23:59:37 2001 +0100
     3.2 +++ b/src/Cube/Base.thy	Fri Nov 09 00:00:53 2001 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4    "Pi x:A. B"   => "Prod(A, %x. B)"
     3.5    "A -> B"      => "Prod(A, _K(B))"
     3.6  
     3.7 -syntax (symbols)
     3.8 +syntax (xsymbols)
     3.9    Trueprop      :: "[context, typing] => prop"          ("(_/ \\<turnstile> _)")
    3.10    box           :: "term"                               ("\\<box>")
    3.11    Lam           :: "[idt, term, term] => term"          ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10)