| #
52683bb6 |
|
04-Jun-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Numerous fixes for theorem-prover example for tight equality
|
| #
55e2defc |
|
04-May-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix theorem-prover/lisp-runtime for new by
|
| #
0697c0a5 |
|
04-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix lisp-runtime/implementation theories for pat_assum
|
| #
9c6f369c |
|
14-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
IN_LIST_TO_SET has been removed.
|
| #
7ac3be79 |
|
25-Oct-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Minor changes towards getting theorem-prover example to build.
Problem is use of IN_DEF as a rewrite when there are also MEM h t
terms around. This is pretty bad form in my opinion, so I don't feel
too bad about having to adjust proofs.
|
| #
07619a09 |
|
19-Jan-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
A mechanised soundness proof for a reflective theorem prover.
|