NEWS
changeset 35763 765f8adf10f9
parent 35745 1416f568b2b6
child 35765 09e238561460
equal deleted inserted replaced
35762:af3ff2ba4c54 35763:765f8adf10f9
    86 * Command 'typedef' now works within a local theory context -- without
    86 * Command 'typedef' now works within a local theory context -- without
    87 introducing dependencies on parameters or assumptions, which is not
    87 introducing dependencies on parameters or assumptions, which is not
    88 possible in Isabelle/Pure/HOL.  Note that the logical environment may
    88 possible in Isabelle/Pure/HOL.  Note that the logical environment may
    89 contain multiple interpretations of local typedefs (with different
    89 contain multiple interpretations of local typedefs (with different
    90 non-emptiness proofs), even in a global theory context.
    90 non-emptiness proofs), even in a global theory context.
       
    91 
       
    92 * Theory Library/Coinductive_List has been removed -- superceded by
       
    93 AFP/thys/Coinductive.
    91 
    94 
    92 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
    95 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
    93 Min, Max from theory Finite_Set.  INCOMPATIBILITY.
    96 Min, Max from theory Finite_Set.  INCOMPATIBILITY.
    94 
    97 
    95 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
    98 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.