changeset 69605 | a96320074298 |
parent 66992 | 69673025292e |
69604:d80b2df54d31 | 69605:a96320074298 |
---|---|
1 theory Proc1 |
1 theory Proc1 |
2 imports "HOL-SPARK.SPARK" |
2 imports "HOL-SPARK.SPARK" |
3 begin |
3 begin |
4 |
4 |
5 spark_open "loop_invariant/proc1" |
5 spark_open \<open>loop_invariant/proc1\<close> |
6 |
6 |
7 spark_vc procedure_proc1_5 |
7 spark_vc procedure_proc1_5 |
8 by (simp add: ring_distribs mod_simps) |
8 by (simp add: ring_distribs mod_simps) |
9 |
9 |
10 spark_vc procedure_proc1_8 |
10 spark_vc procedure_proc1_8 |