| changeset 37848 | a33ecf47f0a0 |
| parent 37296 | 1fad5b94c0ae |
| child 38447 | f55e77f623ab |
--- a/src/HOL/Extraction/ROOT.ML Sun Jul 18 17:56:04 2010 +0200 +++ b/src/HOL/Extraction/ROOT.ML Mon Jul 19 08:59:43 2010 +0200 @@ -1,4 +1,4 @@ (* Examples for program extraction in Higher-Order Logic *) -no_document use_thys ["Efficient_Nat", "~~/src/HOL/Number_Theory/UniqueFactorization"]; +no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/UniqueFactorization"]; use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];