
diff -r 32963b43a538 -r 939e88e79724 src/HOL/SPARK/Manual/Proc2.thy
--- a/src/HOL/SPARK/Manual/Proc2.thy	Tue Apr 29 22:52:15 2014 +0200
+++ b/src/HOL/SPARK/Manual/Proc2.thy	Wed Apr 30 15:43:44 2014 +0200
@@ -2,7 +2,7 @@
 imports SPARK
 begin
 
-spark_open "loop_invariant/proc2.siv"
+spark_open "loop_invariant/proc2"
 
 spark_vc procedure_proc2_7
   by (simp add: ring_distribs pull_mods)




