changeset 66453 | cc19f7ca2ed6 |
parent 63432 | ba7901e94e7b |
child 69605 | a96320074298 |
--- a/src/HOL/SPARK/SPARK_Setup.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/SPARK/SPARK_Setup.thy Fri Aug 18 20:47:47 2017 +0200 @@ -6,7 +6,7 @@ *) theory SPARK_Setup -imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison" +imports "HOL-Word.Word" "HOL-Word.Bit_Comparison" keywords "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and "spark_open" :: thy_load ("siv", "fdl", "rls") and