author | wenzelm |
Thu, 06 Mar 2014 22:15:01 +0100 | |
changeset 55965 | 0c2c61a87a7d |
parent 55085 | 0e8e4dc55866 |
child 55968 | 94242fa87638 |
permissions | -rw-r--r-- |
(* 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