NEWS (changeset 69b35a75caf3): document changes in FuncSet
authorhoelzl
Wed Nov 21 10:48:22 2012 +0100 (2012-11-21)
changeset 501397eb626617bbe
parent 50138 ca989d793b34
child 50140 74773e3dc85d
NEWS (changeset 69b35a75caf3): document changes in FuncSet
NEWS
     1.1 --- a/NEWS	Wed Nov 21 09:07:41 2012 +0100
     1.2 +++ b/NEWS	Wed Nov 21 10:48:22 2012 +0100
     1.3 @@ -201,6 +201,23 @@
     1.4  * Library/Debug.thy and Library/Parallel.thy: debugging and parallel
     1.5  execution for code generated towards Isabelle/ML.
     1.6  
     1.7 +* Library/FuncSet.thy: Extended support for Pi and extensional and introduce the
     1.8 +extensional dependent function space "PiE". Replaces extensional_funcset by an
     1.9 +abbreviation, rename a couple of lemmas from extensional_funcset to PiE:
    1.10 +
    1.11 +      extensional_empty ~> PiE_empty
    1.12 +      extensional_funcset_empty_domain ~> PiE_empty_domain
    1.13 +      extensional_funcset_empty_range ~> PiE_empty_range
    1.14 +      extensional_funcset_arb ~> PiE_arb
    1.15 +      extensional_funcset_mem > PiE_mem
    1.16 +      extensional_funcset_extend_domainI ~> PiE_fun_upd
    1.17 +      extensional_funcset_restrict_domain ~> fun_upd_in_PiE
    1.18 +      extensional_funcset_extend_domain_eq ~> PiE_insert_eq
    1.19 +      card_extensional_funcset ~> card_PiE
    1.20 +      finite_extensional_funcset ~> finite_PiE
    1.21 +
    1.22 +  INCOMPATIBUILITY.
    1.23 +
    1.24  * Library/FinFun.thy: theory of almost everywhere constant functions
    1.25  (supersedes the AFP entry "Code Generation for Functions as Data").
    1.26