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