summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesLib.sml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Make progress on the proofs of the hash mapSon Ho1-2/+2
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho1-4/+35
2023-06-04Make the theorems used by the progress tactic persistentSon Ho1-104/+113
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