isabelle: src/HOL/Extraction/ROOT.ML@ed7bced29e1b (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";
ae4a8446df16 New case study: pigeonhole principle. berghofe parents: 13405 diff changeset	14	no_document time_use_thy "EfficientNat";
ae4a8446df16 New case study: pigeonhole principle. berghofe parents: 13405 diff changeset	15	time_use_thy "Pigeonhole");

author	ballarin
	Wed, 19 Jul 2006 19:25:58 +0200
changeset 20168	ed7bced29e1b
parent 17024	ae4a8446df16
child 23854	688a8a7bcd4e
permissions	-rw-r--r--