summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesBaseTacLib.sml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Fix some minor issuesSon Ho1-22/+45
2023-06-04Make the unfolding theorems collection from evalLib persistentSon Ho1-2/+20
2023-06-04Cleanup a bit the HOL4 backend and implement eval_convSon Ho1-2/+1
2023-06-04Introduce fix_exec, an executable version of fixSon Ho1-0/+1
2023-06-04Reimplement DefineDiv with the new fixed point operatorSon Ho1-1/+4
2023-06-04Improve the performance of dependent rewrites by using netsSon Ho1-49/+106
2023-06-04Make more proofs about the hashmap protoSon Ho1-4/+21
2023-06-04Update the hashmap proofs and fix some tacticsSon Ho1-21/+44
2023-06-04Start working on divDefLib for diverging definitionsSon Ho1-18/+81
2023-06-04Reorganize the HOL4 files and fix some issues with the arithmetic proofsSon Ho1-11/+16
2023-06-04Make progress on the standard library for HOL4Son Ho1-4/+89
2023-06-04Cleanup a bitSon Ho1-8/+14
2023-06-04Use lower case in the names for the HOL4 backendSon Ho1-3/+9
2023-06-04Make progress on primitivesScript.sml and experiment a bitSon Ho1-2/+397
2023-06-04Make progress on the primitives library for HOL4Son Ho1-2/+20
2023-06-04Organize a bit the HOL filesSon Ho1-0/+16
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 13:13:28 +0000