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