isabelle: src/HOL/Extraction/ROOT.ML@f6a4da31f2f1 (annotated)

13405 d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	1	(* Title: HOL/Extraction/ROOT.ML
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	2
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	3	Examples for program extraction in Higher-Order Logic.
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	4	*)
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	5
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	6	if HOL_proofs < 2 then
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	7	warning "HOL proof terms required for running extraction examples"
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	8	else
25374 7657a081fcb4 qualified Proofterm.proofs; wenzelm parents: 24104 diff changeset	9	(Proofterm.proofs := 2;
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 25420 diff changeset	10	no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"];
25420 0fe95159787a Added new exampes Greatest_Common_Divisor and Euclid. berghofe parents: 25374 diff changeset	11	use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]);