NEWS
changeset 14008 f843528b9f3c
parent 13995 ab988a7a8a3b
child 14010 32faa7e2e767
     1.1 --- a/NEWS	Mon May 12 13:49:08 2003 +0200
     1.2 +++ b/NEWS	Mon May 12 13:51:50 2003 +0200
     1.3 @@ -49,6 +49,10 @@
     1.4    - No longer aborts on failed congruence proof.  Instead, the
     1.5      congruence is ignored.
     1.6  
     1.7 +* Pure: New generic framework for extracting programs from constructive
     1.8 +  proofs. See HOL/Extraction.thy for an example instantiation, as well
     1.9 +  as HOL/Extraction for some case studies.
    1.10 +
    1.11  * Pure: The main goal of the proof state is no longer shown by default, only
    1.12  the subgoals. This behaviour is controlled by a new flag.
    1.13     PG menu: Isabelle/Isar -> Settings -> Show Main Goal