equal
deleted
inserted
replaced
4 |
4 |
5 header {* Function Definitions and Termination Proofs *} |
5 header {* Function Definitions and Termination Proofs *} |
6 |
6 |
7 theory FunDef |
7 theory FunDef |
8 imports Partial_Function Wellfounded |
8 imports Partial_Function Wellfounded |
|
9 keywords "function" "termination" :: thy_goal and "fun" :: thy_decl |
9 uses |
10 uses |
10 "Tools/prop_logic.ML" |
11 "Tools/prop_logic.ML" |
11 "Tools/sat_solver.ML" |
12 "Tools/sat_solver.ML" |
12 ("Tools/Function/function_common.ML") |
13 ("Tools/Function/function_common.ML") |
13 ("Tools/Function/context_tree.ML") |
14 ("Tools/Function/context_tree.ML") |