equal
deleted
inserted
replaced
4 |
4 |
5 Setup for SPARK/Ada verification environment. |
5 Setup for SPARK/Ada verification environment. |
6 *) |
6 *) |
7 |
7 |
8 theory SPARK_Setup |
8 theory SPARK_Setup |
9 imports "HOL-Word.Word" "HOL-Word.Bit_Comparison" |
9 imports |
|
10 "HOL-Word.Word" |
10 keywords |
11 keywords |
11 "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and |
12 "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and |
12 "spark_open" :: thy_load ("siv", "fdl", "rls") and |
13 "spark_open" :: thy_load ("siv", "fdl", "rls") and |
13 "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and |
14 "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and |
14 "spark_vc" :: thy_goal and |
15 "spark_vc" :: thy_goal and |