Program extraction framework.
authorberghofe
Mon May 12 13:51:50 2003 +0200 (2003-05-12)
changeset 14008f843528b9f3c
parent 14007 8c2b9750628f
child 14009 0d648f24bab4
Program extraction framework.
NEWS
     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