author | wenzelm |
Fri, 03 Nov 2017 13:43:31 +0100 | |
changeset 66992 | 69673025292e |
parent 66453 | cc19f7ca2ed6 |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
45044 | 1 |
theory Proc2 |
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66453
diff
changeset
|
2 |
imports "HOL-SPARK.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/proc2" |
45044 | 6 |
|
7 |
spark_vc procedure_proc2_7 |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
58130
diff
changeset
|
8 |
by (simp add: ring_distribs mod_simps) |
45044 | 9 |
|
10 |
spark_end |
|
11 |
||
12 |
end |