blanchet@55085: (*  Title:      HOL/Fun_Def_Base.thy
blanchet@55085:     Author:     Alexander Krauss, TU Muenchen
blanchet@55085: *)
blanchet@55085: 
blanchet@55085: header {* Function Definition Base *}
blanchet@55085: 
blanchet@55085: theory Fun_Def_Base
blanchet@55085: imports Ctr_Sugar Set Wellfounded
blanchet@55085: begin
blanchet@55085: 
blanchet@55085: ML_file "Tools/Function/function_lib.ML"
blanchet@55085: ML_file "Tools/Function/function_common.ML"
blanchet@55085: ML_file "Tools/Function/context_tree.ML"
blanchet@55085: setup Function_Ctx_Tree.setup
blanchet@55968: ML_file "Tools/Function/sum_tree.ML"
blanchet@55085: 
blanchet@55085: end