src/CTT/CTT.thy
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 21524 7843e2fd14a9
     1.1 --- a/src/CTT/CTT.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/CTT/CTT.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -65,20 +65,21 @@
     1.4    "SUM x:A. B"  == "Sum(A, %x. B)"
     1.5  
     1.6  abbreviation
     1.7 -  Arrow     :: "[t,t]=>t"           (infixr "-->" 30)
     1.8 +  Arrow     :: "[t,t]=>t"  (infixr "-->" 30) where
     1.9    "A --> B == PROD _:A. B"
    1.10 -  Times     :: "[t,t]=>t"           (infixr "*" 50)
    1.11 +abbreviation
    1.12 +  Times     :: "[t,t]=>t"  (infixr "*" 50) where
    1.13    "A * B == SUM _:A. B"
    1.14  
    1.15  notation (xsymbols)
    1.16 -  Elem  ("(_ /\<in> _)" [10,10] 5)
    1.17 -  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    1.18 -  Arrow  (infixr "\<longrightarrow>" 30)
    1.19 +  Elem  ("(_ /\<in> _)" [10,10] 5) and
    1.20 +  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    1.21 +  Arrow  (infixr "\<longrightarrow>" 30) and
    1.22    Times  (infixr "\<times>" 50)
    1.23  
    1.24  notation (HTML output)
    1.25 -  Elem  ("(_ /\<in> _)" [10,10] 5)
    1.26 -  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    1.27 +  Elem  ("(_ /\<in> _)" [10,10] 5) and
    1.28 +  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    1.29    Times  (infixr "\<times>" 50)
    1.30  
    1.31  syntax (xsymbols)