src/HOL/SPARK/Manual/Proc2.thy
changeset 56798 939e88e79724
parent 45044 2fae15f8984d
child 58130 5e9170812356
equal deleted inserted replaced
56797:32963b43a538 56798:939e88e79724
     1 theory Proc2
     1 theory Proc2
     2 imports SPARK
     2 imports SPARK
     3 begin
     3 begin
     4 
     4 
     5 spark_open "loop_invariant/proc2.siv"
     5 spark_open "loop_invariant/proc2"
     6 
     6 
     7 spark_vc procedure_proc2_7
     7 spark_vc procedure_proc2_7
     8   by (simp add: ring_distribs pull_mods)
     8   by (simp add: ring_distribs pull_mods)
     9 
     9 
    10 spark_end
    10 spark_end