| author | haftmann |
| Sun, 29 Jun 2014 18:02:18 +0200 | |
| changeset 57435 | 312660c1a70a |
| parent 56798 | 939e88e79724 |
| child 58130 | 5e9170812356 |
| permissions | -rw-r--r-- |
| 45044 | 1 |
theory Proc2 |
2 |
imports SPARK |
|
3 |
begin |
|
4 |
||
|
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
45044
diff
changeset
|
5 |
spark_open "loop_invariant/proc2" |
| 45044 | 6 |
|
7 |
spark_vc procedure_proc2_7 |
|
8 |
by (simp add: ring_distribs pull_mods) |
|
9 |
||
10 |
spark_end |
|
11 |
||
12 |
end |