equal
deleted
inserted
replaced
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 nonemptiness proofs), even in a global theory context. 
90 nonemptiness 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. 