src/HOL/Proofs/Extraction/ROOT.ML
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39157 b98909faaea8
child 45047 3aa8d3c391a4
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (* Examples for program extraction in Higher-Order Logic *)
     2 
     3 no_document use_thys [
     4   "~~/src/HOL/Library/Efficient_Nat",
     5   "~~/src/HOL/Library/Monad_Syntax",
     6   "~~/src/HOL/Number_Theory/Primes"
     7 ];
     8 
     9 share_common_data ();
    10 
    11 no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
    12 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];