Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Program extraction framework.
authorberghofe
Mon, 12 May 2003 13:51:50 +0200
changeset 14008 f843528b9f3c
parent 14007 8c2b9750628f
child 14009 0d648f24bab4
Program extraction framework.
NEWS file | annotate | diff | comparison | revisions 
--- 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
isabelle