summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesLib.sml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Make the unfolding theorems collection from evalLib persistentSon Ho1-0/+15
2023-06-04Cleanup a bit the HOL4 backend and implement eval_convSon Ho1-4/+1
2023-06-04Improve the performance of dependent rewrites by using netsSon Ho1-9/+14
2023-06-04Start working on divDefLib for diverging definitionsSon Ho1-45/+0
2023-06-04Reorganize the HOL4 files and fix some issues with the arithmetic proofsSon Ho1-2/+550
2023-06-04Organize a bit the HOL filesSon Ho1-0/+9