Added new exampes Greatest_Common_Divisor and Euclid.

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