isabelle: src/HOL/Extraction/ROOT.ML@d2d7874648bd (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	ID: $Id$
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	3
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	4	Examples for program extraction in Higher-Order Logic.
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	5	*)
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	6
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	7	if HOL_proofs < 2 then
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	8	warning "HOL proof terms required for running extraction examples"
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	9	else
25374 7657a081fcb4 qualified Proofterm.proofs; wenzelm parents: 24104 diff changeset	10	(Proofterm.proofs := 2;
25420 0fe95159787a Added new exampes Greatest_Common_Divisor and Euclid. berghofe parents: 25374 diff changeset	11	no_document use_thys ["Efficient_Nat", "~~/src/HOL/NumberTheory/Factorization"];
0fe95159787a Added new exampes Greatest_Common_Divisor and Euclid. berghofe parents: 25374 diff changeset	12	use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]);

author	wenzelm
	Mon, 16 Mar 2009 18:24:30 +0100
changeset 30549	d2d7874648bd
parent 25420	0fe95159787a
child 32479	521cc9bf2958
permissions	-rw-r--r--