src/CTT/CTT.thy
changeset 21210 c17fd2df4e9e
parent 19761 5cd82054c2c6
child 21404 eb85850d3eb7
     1.1 --- a/src/CTT/CTT.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/CTT/CTT.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -70,13 +70,13 @@
     1.4    Times     :: "[t,t]=>t"           (infixr "*" 50)
     1.5    "A * B == SUM _:A. B"
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    Elem  ("(_ /\<in> _)" [10,10] 5)
    1.10    Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    1.11    Arrow  (infixr "\<longrightarrow>" 30)
    1.12    Times  (infixr "\<times>" 50)
    1.13  
    1.14 -const_syntax (HTML output)
    1.15 +notation (HTML output)
    1.16    Elem  ("(_ /\<in> _)" [10,10] 5)
    1.17    Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    1.18    Times  (infixr "\<times>" 50)