summaryrefslogtreecommitdiff
path: root/backends/hol4/testScript.sml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Start working on divDefLib for diverging definitionsSon Ho1-4/+5
2023-06-04Make progress on primitivesScript.sml and experiment a bitSon Ho1-4/+4
2023-06-04Organize a bit the HOL filesSon Ho1-1/+1
2023-06-04Add a HolmakefileSon Ho1-11/+8
2023-06-04Start working on Primitives.smlSon Ho1-5/+2
2023-06-04Add a more interesting exampleSon Ho1-1/+69
2023-06-04Implement a progress tacticSon Ho1-33/+339
2023-06-04Make more progress on the automationSon Ho1-51/+199
2023-06-04Make minor modifications to the HOL experimentSon Ho1-5/+25
2023-06-04Make progress on implementing tacticsSon Ho1-27/+347
2023-06-04Implement [assume_bounds_for_all_int_vars] to improve the proof experienceSon Ho1-80/+145
2023-06-04Start making tests in HOL4Son Ho1-0/+825