# HG changeset patch
# User hoelzl
# Date 1353491302 -3600
# Node ID 7eb626617bbef8599b9b2a0c48f017b050dc83e3
# Parent  ca989d793b34f27dcb8b99525eaf1191c95e44bf
NEWS (changeset 69b35a75caf3): document changes in FuncSet

diff -r ca989d793b34 -r 7eb626617bbe NEWS
--- a/NEWS	Wed Nov 21 09:07:41 2012 +0100
+++ b/NEWS	Wed Nov 21 10:48:22 2012 +0100
@@ -201,6 +201,23 @@
 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel
 execution for code generated towards Isabelle/ML.
 
+* Library/FuncSet.thy: Extended support for Pi and extensional and introduce the
+extensional dependent function space "PiE". Replaces extensional_funcset by an
+abbreviation, rename a couple of lemmas from extensional_funcset to PiE:
+
+      extensional_empty ~> PiE_empty
+      extensional_funcset_empty_domain ~> PiE_empty_domain
+      extensional_funcset_empty_range ~> PiE_empty_range
+      extensional_funcset_arb ~> PiE_arb
+      extensional_funcset_mem > PiE_mem
+      extensional_funcset_extend_domainI ~> PiE_fun_upd
+      extensional_funcset_restrict_domain ~> fun_upd_in_PiE
+      extensional_funcset_extend_domain_eq ~> PiE_insert_eq
+      card_extensional_funcset ~> card_PiE
+      finite_extensional_funcset ~> finite_PiE
+
+  INCOMPATIBUILITY.
+
 * Library/FinFun.thy: theory of almost everywhere constant functions
 (supersedes the AFP entry "Code Generation for Functions as Data").