# HG changeset patch
# User wenzelm
# Date 1606602625 -3600
# Node ID 47ffeb3448f46481889e139e1b89b797dcc823bc
# Parent  f34f5c057c9ee1c5bcf292323734089429674e94
tuned whitespace;

diff -r f34f5c057c9e -r 47ffeb3448f4 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Sat Nov 28 23:28:56 2020 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Sat Nov 28 23:30:25 2020 +0100
@@ -6,14 +6,12 @@
 *)
 
 theory SPARK_Setup
-  imports
-  "HOL-Library.Word"
-keywords
-  "spark_open_vcg" :: thy_load (spark_vcg) and
-  "spark_open" :: thy_load (spark_siv) and
-  "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
-  "spark_vc" :: thy_goal and
-  "spark_status" :: diag
+  imports "HOL-Library.Word"
+  keywords "spark_open_vcg" :: thy_load (spark_vcg)
+    and "spark_open" :: thy_load (spark_siv)
+    and "spark_proof_functions" "spark_types" "spark_end" :: thy_decl
+    and "spark_vc" :: thy_goal
+    and "spark_status" :: diag
 begin
 
 ML_file \<open>Tools/fdl_lexer.ML\<close>