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.
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
authorwenzelm
Mon, 16 Aug 2010 22:56:28 +0200
changeset 38447 f55e77f623ab
parent 38446 9d59dab38fef
child 38448 62d16c415019
child 38450 ada5814c9d87
child 38452 abc655166d61
HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
src/HOL/Extraction/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction/ROOT.ML	Mon Aug 16 18:20:36 2010 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Mon Aug 16 22:56:28 2010 +0200
@@ -1,4 +1,6 @@
 (* Examples for program extraction in Higher-Order Logic *)
 
-no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/UniqueFactorization"];
+no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"];
+share_common_data ();
+no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
isabelle