| #
52683bb6 |
|
04-Jun-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Numerous fixes for theorem-prover example for tight equality
|
| #
4b814b28 |
|
06-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix code in theorem-prover + machine-code ex's for remove-term-eqtype
|
| #
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
|
| #
af4c68dd |
|
17-Sep-2012 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
split lisp_symbols into separate files
|
| #
e478432c |
|
15-Sep-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Attempt to patch broken theorem-prover example.
EVAL will no longer do anything with the term ``EVAL n (x::xs)``.
|
| #
07619a09 |
|
19-Jan-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
A mechanised soundness proof for a reflective theorem prover.
|