--- a/src/HOL/SPARK/SPARK_Setup.thy Fri Nov 27 21:59:23 2020 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy Fri Nov 27 23:47:06 2020 +0100
@@ -9,8 +9,8 @@
imports
"HOL-Library.Word"
keywords
- "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
- "spark_open" :: thy_load ("siv", "fdl", "rls") and
+ "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