src/HOL/SPARK/Manual/Proc1.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Manual/Proc1.thy	Thu Sep 22 16:50:23 2011 +0200
@@ -0,0 +1,18 @@
+theory Proc1
+imports SPARK
+begin
+
+spark_open "loop_invariant/proc1.siv"
+
+spark_vc procedure_proc1_5
+  by (simp add: ring_distribs pull_mods)
+
+spark_vc procedure_proc1_8
+  by (simp add: ring_distribs pull_mods)
+
+spark_end
+
+lemma pow_2_32_simp: "4294967296 = (2::int)^32"
+  by simp
+
+end