1theory Proc2 2imports "HOL-SPARK.SPARK" 3begin 4 5spark_open \<open>loop_invariant/proc2\<close> 6 7spark_vc procedure_proc2_7 8 by (simp add: ring_distribs mod_simps) 9 10spark_end 11 12end 13