src/CTT/CTT.thy
 changeset 21404 eb85850d3eb7 parent 21210 c17fd2df4e9e child 21524 7843e2fd14a9
equal 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)`