changeset 13405 | d20a4e67afc8 |
child 17024 | ae4a8446df16 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/ROOT.ML Sun Jul 21 15:44:42 2002 +0200 @@ -0,0 +1,13 @@ +(* Title: HOL/Extraction/ROOT.ML + ID: $Id$ + +Examples for program extraction in Higher-Order Logic. +*) + +if HOL_proofs < 2 then + warning "HOL proof terms required for running extraction examples" +else + (proofs := 2; + time_use_thy "QuotRem"; + time_use_thy "Warshall"; + time_use_thy "Higman");