src/HOL/Fun_Def.thy
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>