isabelle: src/HOL/Extraction/ROOT.ML@cbad32e7ab40 (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
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	10	(proofs := 2;
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	11	time_use_thy "QuotRem";
d20a4e67afc8 Examples for program extraction in HOL. berghofe parents: diff changeset	12	time_use_thy "Warshall";
17024 ae4a8446df16 New case study: pigeonhole principle. berghofe parents: 13405 diff changeset	13	time_use_thy "Higman";
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 17024 diff changeset	14	no_document time_use_thy "Efficient_Nat";
17024 ae4a8446df16 New case study: pigeonhole principle. berghofe parents: 13405 diff changeset	15	time_use_thy "Pigeonhole");

author	wenzelm
	Tue, 31 Jul 2007 13:30:35 +0200
changeset 24085	cbad32e7ab40
parent 23854	688a8a7bcd4e
child 24104	719fbe4fb77f
permissions	-rw-r--r--