# HG changeset patch
# User berghofe
# Date 1194947754 -3600
# Node ID 0fe95159787a020c0fed7a17afa0f9fb589aab65
# Parent  e6a56be0ccaa342955d9b2d4967650f7dfb792b1
Added new exampes Greatest_Common_Divisor and Euclid.

diff -r e6a56be0ccaa -r 0fe95159787a src/HOL/Extraction/ROOT.ML
--- a/src/HOL/Extraction/ROOT.ML	Tue Nov 13 10:55:08 2007 +0100
+++ b/src/HOL/Extraction/ROOT.ML	Tue Nov 13 10:55:54 2007 +0100
@@ -8,5 +8,5 @@
   warning "HOL proof terms required for running extraction examples"
 else
   (Proofterm.proofs := 2;
-   no_document time_use_thy "Efficient_Nat";
-   use_thys ["QuotRem", "Warshall", "Higman", "Pigeonhole"]);
+   no_document use_thys ["Efficient_Nat", "~~/src/HOL/NumberTheory/Factorization"];
+   use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]);