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;
wenzelm@34205
     1
(* Examples for program extraction in Higher-Order Logic *)
berghofe@13405
     2
wenzelm@41413
     3
no_document use_thys [
wenzelm@41413
     4
  "~~/src/HOL/Library/Efficient_Nat",
wenzelm@41413
     5
  "~~/src/HOL/Library/Monad_Syntax",
wenzelm@41413
     6
  "~~/src/HOL/Number_Theory/Primes"
wenzelm@41413
     7
];
wenzelm@41413
     8
wenzelm@38447
     9
share_common_data ();
wenzelm@41413
    10
wenzelm@38447
    11
no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
wenzelm@34205
    12
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];