src/HOL/Recdef.thy
changeset 38554 f8999e19dd49
parent 37767 a2b7a20d6ea3
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Recdef.thy	Thu Aug 19 12:11:57 2010 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Thu Aug 19 16:03:01 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* TFL: recursive function definitions *}
     1.5  
     1.6  theory Recdef
     1.7 -imports FunDef Plain
     1.8 +imports Plain Hilbert_Choice
     1.9  uses
    1.10    ("Tools/TFL/casesplit.ML")
    1.11    ("Tools/TFL/utils.ML")