| author | blanchet |
| Mon, 29 Sep 2014 10:39:39 +0200 | |
| changeset 58476 | 6ade4c7109a8 |
| parent 58130 | 5e9170812356 |
| child 64593 | 50c715579715 |
| permissions | -rw-r--r-- |
| 45044 | 1 |
theory Proc1 |
| 58130 | 2 |
imports "../SPARK" |
| 45044 | 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/proc1" |
| 45044 | 6 |
|
7 |
spark_vc procedure_proc1_5 |
|
8 |
by (simp add: ring_distribs pull_mods) |
|
9 |
||
10 |
spark_vc procedure_proc1_8 |
|
11 |
by (simp add: ring_distribs pull_mods) |
|
12 |
||
13 |
spark_end |
|
14 |
||
15 |
lemma pow_2_32_simp: "4294967296 = (2::int)^32" |
|
16 |
by simp |
|
17 |
||
18 |
end |