NEWS
changeset 35745 1416f568b2b6
parent 35728 c36ade6f4c33
child 35763 765f8adf10f9
equal deleted inserted replaced
35744:93603d7b8ee9 35745:1416f568b2b6
    80 without introducing dependencies on parameters or assumptions, which
    80 without introducing dependencies on parameters or assumptions, which
    81 is not possible in Isabelle/Pure.
    81 is not possible in Isabelle/Pure.
    82 
    82 
    83 
    83 
    84 *** HOL ***
    84 *** HOL ***
       
    85 
       
    86 * Command 'typedef' now works within a local theory context -- without
       
    87 introducing dependencies on parameters or assumptions, which is not
       
    88 possible in Isabelle/Pure/HOL.  Note that the logical environment may
       
    89 contain multiple interpretations of local typedefs (with different
       
    90 non-emptiness proofs), even in a global theory context.
    85 
    91 
    86 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
    92 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
    87 Min, Max from theory Finite_Set.  INCOMPATIBILITY.
    93 Min, Max from theory Finite_Set.  INCOMPATIBILITY.
    88 
    94 
    89 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
    95 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.