#
66d88b8c |
|
29-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix computability thy's in light of pat_assum rename
|
#
2237e792 |
|
10-Nov-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Fix goedelCode example (broken by 5203fc450fa I assume).
|
#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
7b73c8d7 |
|
16-Jul-2010 |
Konrad Slind <konrad.slind@gmail.com> |
src/num/theories/SingleStep.{sig,sml} is gone. The defininitions of Cases, Cases_on, Induct, Induct_on, CASE_TAC (and co.) are now in basicProof/BasicProvers. completeInduct_on and measureInduct_on are now in numLib. recInduct is now in src/tfl/Induction.sml. All these are collected in bossLib, so the changes should be invisible to ordinary users. SingleStep.*.doc has been changed accordingly. BasicProvers.NORM_TAC should now automatically perform all case splits (from if-then-else expressions as well as case expression) arising anywhere in the goal.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
04184e04 |
|
11-May-2009 |
Konrad Slind <konrad.slind@gmail.com> |
Added decoder for Goedel numbers.
|
#
5bec6803 |
|
05-May-2009 |
Konrad Slind <konrad.slind@gmail.com> |
Goedel coding of number lists. To be used to encode register and Turing machines.
|