src/HOL/Proofs/Extraction/ROOT.ML
author wenzelm
Tue, 17 Jul 2012 13:07:28 +0200
changeset 48274 c8dce1689f79
parent 45047 3aa8d3c391a4
permissions -rw-r--r--
avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 32479
diff changeset
     1
(* Examples for program extraction in Higher-Order Logic *)
13405
d20a4e67afc8 Examples for program extraction in HOL.
berghofe
parents:
diff changeset
     2
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39157
diff changeset
     3
no_document use_thys [
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39157
diff changeset
     4
  "~~/src/HOL/Library/Efficient_Nat",
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39157
diff changeset
     5
  "~~/src/HOL/Library/Monad_Syntax",
48274
c8dce1689f79 avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);
wenzelm
parents: 45047
diff changeset
     6
  "~~/src/HOL/Number_Theory/Primes",
c8dce1689f79 avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);
wenzelm
parents: 45047
diff changeset
     7
  "~~/src/HOL/Number_Theory/UniqueFactorization",
c8dce1689f79 avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);
wenzelm
parents: 45047
diff changeset
     8
  "~~/src/HOL/Library/State_Monad"
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39157
diff changeset
     9
];
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39157
diff changeset
    10
45047
3aa8d3c391a4 Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents: 41413
diff changeset
    11
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"];