| changeset 56798 | 939e88e79724 |
| parent 45044 | 2fae15f8984d |
| child 58130 | 5e9170812356 |
| 56797:32963b43a538 | 56798:939e88e79724 |
|---|---|
1 theory Proc1 |
1 theory Proc1 |
2 imports SPARK |
2 imports SPARK |
3 begin |
3 begin |
4 |
4 |
5 spark_open "loop_invariant/proc1.siv" |
5 spark_open "loop_invariant/proc1" |
6 |
6 |
7 spark_vc procedure_proc1_5 |
7 spark_vc procedure_proc1_5 |
8 by (simp add: ring_distribs pull_mods) |
8 by (simp add: ring_distribs pull_mods) |
9 |
9 |
10 spark_vc procedure_proc1_8 |
10 spark_vc procedure_proc1_8 |