| #
ee0a2108 |
|
21-Jul-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fix proof broken by abbrev changes
|
| #
3191ad20 |
|
25-May-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fix proof broken by 508f79ea9 and 8ab15c2ff
|
| #
5b71417e |
|
10-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix milawa-prover files for remove-term-eqtype
|
| #
ee0d6faf |
|
04-May-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix milawa-prover (all of theorem-prover now builds) for new by
|
| #
771a174d |
|
07-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Finish theorem-prover example for pat_assum rename
|
| #
9c6f369c |
|
14-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
IN_LIST_TO_SET has been removed.
|
| #
a3b3ff4d |
|
23-Oct-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Attempt fix for Milawa example.
The constant INDEX_OF is now in listTheory (but there the "n" argument is dropped through being specialised to 0).
|
| #
6791cfd1 |
|
26-Jul-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
double 'the' removed
|
| #
b9f664ff |
|
01-Oct-2012 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
fixed broken proof
|
| #
a6ef9ed4 |
|
04-May-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
More fixes following change to tDefine.
|
| #
1cbb37d8 |
|
21-Apr-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
Improved top-level soundness theorem
|
| #
47895016 |
|
20-Apr-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
Simplified the definition of the semantics.
|
| #
e66d583a |
|
11-Feb-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
New examples: code synthesis and evaluation through reflection
|
| #
2b2de9e4 |
|
25-Jan-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
Minor edits following some paper writing.
|
| #
07619a09 |
|
19-Jan-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
A mechanised soundness proof for a reflective theorem prover.
|