src/HOL/SPARK/Manual/Proc2.thy
changeset 66453 cc19f7ca2ed6
parent 64593 50c715579715
child 66992 69673025292e
equal deleted inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6
     1 theory Proc2
     1 theory Proc2
     2 imports "../SPARK"
     2 imports SPARK
     3 begin
     3 begin
     4 
     4 
     5 spark_open "loop_invariant/proc2"
     5 spark_open "loop_invariant/proc2"
     6 
     6 
     7 spark_vc procedure_proc2_7
     7 spark_vc procedure_proc2_7