# HG changeset patch
# User wenzelm
# Date 1468223840 -7200
# Node ID ba7901e94e7bfa75aa752447490ec30fedd0b876
# Parent  8002eec44fbb811fb9a785e11453dbcc4f58cf8c
tuned;

diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/Fun_Def.thy
--- 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>
diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/HOL/HOLCF/Domain.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -7,8 +7,8 @@
 theory Domain
 imports Representable Domain_Aux
 keywords
-  "domaindef" :: thy_decl and "lazy" "unsafe" and
-  "domain_isomorphism" "domain" :: thy_decl
+  "lazy" "unsafe" and
+  "domaindef" "domain_isomorphism" "domain" :: thy_decl
 begin
 
 default_sort "domain"
diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/Library/Refute.thy
--- a/src/HOL/Library/Refute.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/HOL/Library/Refute.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -9,7 +9,9 @@
 
 theory Refute
 imports Main
-keywords "refute" :: diag and "refute_params" :: thy_decl
+keywords
+  "refute" :: diag and
+  "refute_params" :: thy_decl
 begin
 
 ML_file "refute.ML"
diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/Library/Simps_Case_Conv.thy
--- a/src/HOL/Library/Simps_Case_Conv.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -3,8 +3,10 @@
 *)
 
 theory Simps_Case_Conv
-  imports Main
-  keywords "simps_of_case" :: thy_decl == "" and "case_of_simps" :: thy_decl
+imports Main
+keywords
+  "simps_of_case" :: thy_decl == "" and
+  "case_of_simps" :: thy_decl
 begin
 
 ML_file "simps_case_conv.ML"
diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/HOL/Predicate_Compile.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -6,7 +6,9 @@
 
 theory Predicate_Compile
 imports Random_Sequence Quickcheck_Exhaustive
-keywords "code_pred" :: thy_goal and "values" :: diag
+keywords
+  "code_pred" :: thy_goal and
+  "values" :: diag
 begin
 
 ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -11,7 +11,8 @@
   "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
   "spark_open" :: thy_load ("siv", "fdl", "rls") and
   "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
-  "spark_vc" :: thy_goal and "spark_status" :: diag
+  "spark_vc" :: thy_goal and
+  "spark_status" :: diag
 begin
 
 ML_file "Tools/fdl_lexer.ML"
diff -r 8002eec44fbb -r ba7901e94e7b src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -8,7 +8,9 @@
 
 theory Sledgehammer
 imports Presburger SMT
-keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
+keywords
+  "sledgehammer" :: diag and
+  "sledgehammer_params" :: thy_decl
 begin
 
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
diff -r 8002eec44fbb -r ba7901e94e7b src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy	Mon Jul 11 09:45:10 2016 +0200
+++ b/src/Tools/Adhoc_Overloading.thy	Mon Jul 11 09:57:20 2016 +0200
@@ -6,7 +6,8 @@
 
 theory Adhoc_Overloading
 imports Pure
-keywords "adhoc_overloading" :: thy_decl and  "no_adhoc_overloading" :: thy_decl
+keywords
+  "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
 begin
 
 ML_file "adhoc_overloading.ML"