summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

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);

--- 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"];