changeset 24162 | 8dfd5dd65d82 |
parent 23739 | c5ead5df7f35 |
child 24194 | 96013f81faef |
--- a/src/HOL/FunDef.thy Tue Aug 07 09:38:43 2007 +0200 +++ b/src/HOL/FunDef.thy Tue Aug 07 09:38:44 2007 +0200 @@ -6,7 +6,7 @@ header {* General recursive function definitions *} theory FunDef -imports Datatype Accessible_Part +imports Datatype Option Accessible_Part uses ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/fundef_common.ML")