# HG changeset patch
# User berghofe
# Date 1052740310 -7200
# Node ID f843528b9f3c7c3bf6e3cbaf0a47beea339ff29f
# Parent  8c2b9750628f00e090e39f43c22c305c8c3bc6a6
Program extraction framework.

diff -r 8c2b9750628f -r f843528b9f3c NEWS
--- a/NEWS	Mon May 12 13:49:08 2003 +0200
+++ b/NEWS	Mon May 12 13:51:50 2003 +0200
@@ -49,6 +49,10 @@
   - No longer aborts on failed congruence proof.  Instead, the
     congruence is ignored.
 
+* Pure: New generic framework for extracting programs from constructive
+  proofs. See HOL/Extraction.thy for an example instantiation, as well
+  as HOL/Extraction for some case studies.
+
 * Pure: The main goal of the proof state is no longer shown by default, only
 the subgoals. This behaviour is controlled by a new flag.
    PG menu: Isabelle/Isar -> Settings -> Show Main Goal