Add alternative imperative example and proofs of equivalence with fun-op-sem/imp

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

https://hol-theorem-prover.org

Other

630 stars 142 forks source link

Add alternative imperative example and proofs of equivalence with fun-op-sem/imp #1321

Closed adamstucci closed 4 weeks ago