author | wenzelm |
Wed, 29 Dec 2010 17:34:41 +0100 | |
changeset 41413 | 64cd30d6b0b8 |
parent 39157 | b98909faaea8 |
child 45047 | 3aa8d3c391a4 |
permissions | -rw-r--r-- |
(* Examples for program extraction in Higher-Order Logic *) no_document use_thys [ "~~/src/HOL/Library/Efficient_Nat", "~~/src/HOL/Library/Monad_Syntax", "~~/src/HOL/Number_Theory/Primes" ]; share_common_data (); no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"]; use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];