#
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.
|