src/CTT/CTT.thy
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 21524 7843e2fd14a9
equal deleted inserted replaced
21403:dd58f13a8eb4 21404:eb85850d3eb7
    63 translations
    63 translations
    64   "PROD x:A. B" == "Prod(A, %x. B)"
    64   "PROD x:A. B" == "Prod(A, %x. B)"
    65   "SUM x:A. B"  == "Sum(A, %x. B)"
    65   "SUM x:A. B"  == "Sum(A, %x. B)"
    66 
    66 
    67 abbreviation
    67 abbreviation
    68   Arrow     :: "[t,t]=>t"           (infixr "-->" 30)
    68   Arrow     :: "[t,t]=>t"  (infixr "-->" 30) where
    69   "A --> B == PROD _:A. B"
    69   "A --> B == PROD _:A. B"
    70   Times     :: "[t,t]=>t"           (infixr "*" 50)
    70 abbreviation
       
    71   Times     :: "[t,t]=>t"  (infixr "*" 50) where
    71   "A * B == SUM _:A. B"
    72   "A * B == SUM _:A. B"
    72 
    73 
    73 notation (xsymbols)
    74 notation (xsymbols)
    74   Elem  ("(_ /\<in> _)" [10,10] 5)
    75   Elem  ("(_ /\<in> _)" [10,10] 5) and
    75   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    76   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    76   Arrow  (infixr "\<longrightarrow>" 30)
    77   Arrow  (infixr "\<longrightarrow>" 30) and
    77   Times  (infixr "\<times>" 50)
    78   Times  (infixr "\<times>" 50)
    78 
    79 
    79 notation (HTML output)
    80 notation (HTML output)
    80   Elem  ("(_ /\<in> _)" [10,10] 5)
    81   Elem  ("(_ /\<in> _)" [10,10] 5) and
    81   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    82   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    82   Times  (infixr "\<times>" 50)
    83   Times  (infixr "\<times>" 50)
    83 
    84 
    84 syntax (xsymbols)
    85 syntax (xsymbols)
    85   "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    86   "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    86   "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    87   "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)