author wenzelm
Wed, 02 Jun 2010 21:12:28 +0200
changeset 37296 1fad5b94c0ae
parent 37288 2b1c6dd48995
child 37848 a33ecf47f0a0
permissions -rw-r--r--
replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;

(* Examples for program extraction in Higher-Order Logic *)

no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"];
use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];