--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Fun_Def_Base.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Fun_Def_Base.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+header {* Function Definition Base *}
+
+theory Fun_Def_Base
+imports Ctr_Sugar Set Wellfounded
+begin
+
+ML_file "Tools/Function/function_lib.ML"
+ML_file "Tools/Function/function_common.ML"
+ML_file "Tools/Function/context_tree.ML"
+setup Function_Ctx_Tree.setup
+
+end