src/HOL/Proofs/Extraction/ROOT.ML
changeset 41413 64cd30d6b0b8
parent 39157 b98909faaea8
child 45047 3aa8d3c391a4
     1.1 --- a/src/HOL/Proofs/Extraction/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Proofs/Extraction/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -1,6 +1,12 @@
     1.4  (* Examples for program extraction in Higher-Order Logic *)
     1.5  
     1.6 -no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"];
     1.7 +no_document use_thys [
     1.8 +  "~~/src/HOL/Library/Efficient_Nat",
     1.9 +  "~~/src/HOL/Library/Monad_Syntax",
    1.10 +  "~~/src/HOL/Number_Theory/Primes"
    1.11 +];
    1.12 +
    1.13  share_common_data ();
    1.14 +
    1.15  no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
    1.16  use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];