changeset 70172 | c247bf924d25 |
parent 69605 | a96320074298 |
child 72515 | c7038c397ae3 |
--- a/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 16 19:50:07 2019 +0000 +++ b/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 16 19:50:09 2019 +0000 @@ -6,7 +6,8 @@ *) theory SPARK_Setup -imports "HOL-Word.Word" "HOL-Word.Bit_Comparison" + imports + "HOL-Word.Word" keywords "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and "spark_open" :: thy_load ("siv", "fdl", "rls") and