spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants;
theory Proc2
imports SPARK
begin
spark_open "loop_invariant/proc2"
spark_vc procedure_proc2_7
by (simp add: ring_distribs pull_mods)
spark_end
end