src/HOL/Extraction/ROOT.ML

--- a/src/HOL/Extraction/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* Examples for program extraction in Higher-Order Logic *)
-
-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"];