Files
Johannes Kanig a5f8179ccb Fix proof of SPARK library
* generate_session.py
- show proved VC when running Coq; this helps detect when the
  --limit-line argument is incorrect
- delete more files
- remove useless level argument to call of run_automatic
* manual_proof.in: fixed locations of checks
* lemma_raising_order_*.prf: fixed proof of lemma, the proof is now much
  simpler
2023-07-06 11:03:57 +09:00
..
2023-07-06 11:03:57 +09:00
2023-07-06 11:03:57 +09:00