equal
deleted
inserted
replaced
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 |