NEWS
changeset 50232 289a34f9c383
parent 50231 81a067b188b8
child 50406 c28753665b8e
equal deleted inserted replaced
50231:81a067b188b8 50232:289a34f9c383
   238       extensional_funcset_restrict_domain ~> fun_upd_in_PiE
   238       extensional_funcset_restrict_domain ~> fun_upd_in_PiE
   239       extensional_funcset_extend_domain_eq ~> PiE_insert_eq
   239       extensional_funcset_extend_domain_eq ~> PiE_insert_eq
   240       card_extensional_funcset ~> card_PiE
   240       card_extensional_funcset ~> card_PiE
   241       finite_extensional_funcset ~> finite_PiE
   241       finite_extensional_funcset ~> finite_PiE
   242 
   242 
   243   INCOMPATIBUILITY.
   243   INCOMPATIBILITY.
   244 
   244 
   245 * Library/FinFun.thy: theory of almost everywhere constant functions
   245 * Library/FinFun.thy: theory of almost everywhere constant functions
   246 (supersedes the AFP entry "Code Generation for Functions as Data").
   246 (supersedes the AFP entry "Code Generation for Functions as Data").
   247 
   247 
   248 * Library/Phantom.thy: generic phantom type to make a type parameter
   248 * Library/Phantom.thy: generic phantom type to make a type parameter