src/CTT/CTT.thy
changeset 10467 e6e7205e9e91
parent 3837 d7f033c74b38
child 12110 f8b4b11cd79d
     1.1 --- a/src/CTT/CTT.thy	Tue Nov 14 13:25:59 2000 +0100
     1.2 +++ b/src/CTT/CTT.thy	Tue Nov 14 13:26:48 2000 +0100
     1.3 @@ -39,9 +39,9 @@
     1.4    eq        :: "i"
     1.5    (*Judgements*)
     1.6    Type      :: "t => prop"          ("(_ type)" [10] 5)
     1.7 -  Eqtype    :: "[t,t]=>prop"        ("(3_ =/ _)" [10,10] 5)
     1.8 +  Eqtype    :: "[t,t]=>prop"        ("(_ =/ _)" [10,10] 5)
     1.9    Elem      :: "[i, t]=>prop"       ("(_ /: _)" [10,10] 5)
    1.10 -  Eqelem    :: "[i,i,t]=>prop"      ("(3_ =/ _ :/ _)" [10,10,10] 5)
    1.11 +  Eqelem    :: "[i,i,t]=>prop"      ("(_ =/ _ :/ _)" [10,10,10] 5)
    1.12    Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
    1.13    (*Types*)
    1.14    "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    1.15 @@ -64,6 +64,17 @@
    1.16    "SUM x:A. B"  => "Sum(A, %x. B)"
    1.17    "A * B"       => "Sum(A, _K(B))"
    1.18  
    1.19 +syntax (xsymbols)
    1.20 +  "@-->"    :: "[t,t]=>t"           ("(_ \\<longrightarrow>/ _)" [31,30] 30)
    1.21 +  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
    1.22 +
    1.23 +syntax (symbols)
    1.24 +  Elem      :: "[i, t]=>prop"     ("(_ /\\<in> _)" [10,10] 5)
    1.25 +  Eqelem    :: "[i,i,t]=>prop"    ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    1.26 +  "@SUM"    :: "[idt,t,t] => t"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
    1.27 +  "@PROD"   :: "[idt,t,t] => t"   ("(3\\<Pi> _\\<in>_./ _)"    10)
    1.28 +  "lam "    :: "[idts, i] => i"   ("(3\\<lambda>\\<lambda>_./ _)" 10)
    1.29 +
    1.30  rules
    1.31  
    1.32    (*Reduction: a weaker notion than equality;  a hack for simplification.