changeset 63432 | ba7901e94e7b |
parent 61841 | 4d3527b94f2a |
child 63654 | f90e3926e627 |
--- a/src/HOL/Fun_Def.thy Mon Jul 11 09:45:10 2016 +0200 +++ b/src/HOL/Fun_Def.thy Mon Jul 11 09:57:20 2016 +0200 @@ -6,7 +6,9 @@ theory Fun_Def imports Basic_BNF_LFPs Partial_Function SAT -keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl +keywords + "function" "termination" :: thy_goal and + "fun" "fun_cases" :: thy_decl begin subsection \<open>Definitions with default value\<close>