equal
deleted
inserted
replaced
190  Renamed many generated theorems, including 
190  Renamed many generated theorems, including 
191 map_comp' ~> map_comp 
191 map_comp' ~> map_comp 
192 map_id' ~> map_id 
192 map_id' ~> map_id 
193 set_map' ~> set_map 
193 set_map' ~> set_map 
194 IMCOMPATIBILITY. 
194 IMCOMPATIBILITY. 

195 

196 * Function package: For mutually recursive functions f and g, separate 

197 cases rules f.cases and g.cases are generated instead of unusable 

198 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY, 

199 in the case that the unusable rule was used nevertheless. 

200 

201 * Function package: For each function f, new rules f.elims are 

202 automatically generated, which eliminate equalities of the form "f x = 

203 t". 

204 

205 * New command "fun_cases" derives adhoc elimination rules for 

206 function equations as simplified instances of f.elims, analogous to 

207 inductive_cases. See HOL/ex/Fundefs.thy for some examples. 
195 
208 
196 * Library/Polynomial.thy: 
209 * Library/Polynomial.thy: 
197  Use lifting for primitive definitions. 
210  Use lifting for primitive definitions. 
198  Explicit conversions from and to lists of coefficients, used for 
211  Explicit conversions from and to lists of coefficients, used for 
199 generated code. 
212 generated code. 