src/CTT/CTT.thy
changeset 21524 7843e2fd14a9
parent 21404 eb85850d3eb7
child 22808 a7daa74e2980
equal deleted inserted replaced
21523:a267ecd51f90 21524:7843e2fd14a9
    70 abbreviation
    70 abbreviation
    71   Times     :: "[t,t]=>t"  (infixr "*" 50) where
    71   Times     :: "[t,t]=>t"  (infixr "*" 50) where
    72   "A * B == SUM _:A. B"
    72   "A * B == SUM _:A. B"
    73 
    73 
    74 notation (xsymbols)
    74 notation (xsymbols)
       
    75   lambda  (binder "\<lambda>\<lambda>" 10) and
    75   Elem  ("(_ /\<in> _)" [10,10] 5) and
    76   Elem  ("(_ /\<in> _)" [10,10] 5) and
    76   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    77   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    77   Arrow  (infixr "\<longrightarrow>" 30) and
    78   Arrow  (infixr "\<longrightarrow>" 30) and
    78   Times  (infixr "\<times>" 50)
    79   Times  (infixr "\<times>" 50)
    79 
    80 
    80 notation (HTML output)
    81 notation (HTML output)
       
    82   lambda  (binder "\<lambda>\<lambda>" 10) and
    81   Elem  ("(_ /\<in> _)" [10,10] 5) and
    83   Elem  ("(_ /\<in> _)" [10,10] 5) and
    82   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    84   Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    83   Times  (infixr "\<times>" 50)
    85   Times  (infixr "\<times>" 50)
    84 
    86 
    85 syntax (xsymbols)
    87 syntax (xsymbols)
    86   "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    88   "_PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    87   "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    89   "_SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    88   "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
       
    89 
    90 
    90 syntax (HTML output)
    91 syntax (HTML output)
    91   "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    92   "_PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    92   "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    93   "_SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    93   "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
       
    94 
    94 
    95 axioms
    95 axioms
    96 
    96 
    97   (*Reduction: a weaker notion than equality;  a hack for simplification.
    97   (*Reduction: a weaker notion than equality;  a hack for simplification.
    98     Reduce[a,b] means either that  a=b:A  for some A or else that "a" and "b"
    98     Reduce[a,b] means either that  a=b:A  for some A or else that "a" and "b"