equal
deleted
inserted
replaced
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 nonemptiness 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. 