#
8d83067c |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from examples
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
2c912195 |
|
22-Jul-2010 |
Konrad Slind <konrad.slind@gmail.com> |
Synching remote copy. Also, fix to miller build failure (NORM_TAC is more effective than before, breaking the proof).
|
#
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!
|
#
7b11d4a6 |
|
14-Jun-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Added proofManagerLib. This adds a type of "goal trees" as an alternative to goalstacks. Relevant entrypoints: gt ` .... ` -- start a goaltree proof, analogous to g eq ` ... ` -- expand a tactic, analogous to e (except that the text of the tactic is delimited by quotes). A goaltree manages the construction of the final tactic, so should ease some of the script maintenance that the goalstack requires. Backup and restart are just as for goalstacks. All the entrypoints for goalstacks are just as they were before; there shouldn't be any difference.
|
#
7d90547c |
|
29-Mar-2008 |
Konrad Slind <konrad.slind@gmail.com> |
This check-in mainly fixes a problem with literals occurring in patterns of TFL-style definitions. There are a host of other minor changes as well.
|
#
bcca2984 |
|
09-Nov-2007 |
Guodong Li <ligd@cs.utah.edu> |
Refine front-end outputs to be more consistent with Magnus's backend.
|
#
7f72e857 |
|
07-Nov-2007 |
Guodong Li <ligd@cs.utah.edu> |
Connect the front-end and back-end of the software compiler. More refinements are needed for the arm backend to work.
|