changeset 29654 | 24e73987bfe2 |
parent 26748 | 4d51ddd6aa5c |
child 31723 | f5cafe803b55 |
--- a/src/HOL/Recdef.thy Wed Jan 28 11:02:12 2009 +0100 +++ b/src/HOL/Recdef.thy Wed Jan 28 11:03:16 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Recdef.thy - ID: $Id$ Author: Konrad Slind and Markus Wenzel, TU Muenchen *) header {* TFL: recursive function definitions *} theory Recdef -imports FunDef +imports FunDef Plain uses ("Tools/TFL/casesplit.ML") ("Tools/TFL/utils.ML")