| Commit message (Expand) | Author | Files | Lines |
2023-09-07 | Fix some issues | Son Ho | 1 | -0/+120 |
2023-06-04 | Update the HOL4 proofs for the last *release* version of HOL4 | Son Ho | 1 | -113/+113 |
2023-06-04 | Finish the proofs of the hashmap | Son Ho | 1 | -4/+20 |
2023-06-04 | Make good progress on the proofs of the hashmap in HOL4 | Son Ho | 1 | -6/+33 |
2023-06-04 | Make the theorems used by the progress tactic persistent | Son Ho | 1 | -10/+5 |
2023-06-04 | Make progress on the HOL4 backend | Son Ho | 1 | -16/+143 |
2023-06-04 | Make progress on extracting the HOL4 files | Son Ho | 1 | -2/+97 |
2023-06-04 | Update the definitions of mk_vec and vec_insert_back | Son Ho | 1 | -6/+15 |
2023-06-04 | Cleanup a bit the HOL4 backend and implement eval_conv | Son Ho | 1 | -0/+104 |
2023-06-04 | Make good progress on generating code for HOL4 | Son Ho | 1 | -0/+331 |
2023-06-04 | Cleanup a bit and reorganize | Son Ho | 1 | -0/+6 |
2023-06-04 | Start working on divDefLib for diverging definitions | Son Ho | 1 | -11/+11 |
2023-06-04 | Make progress on the standard library for HOL4 | Son Ho | 1 | -2/+2 |
2023-06-04 | Cleanup a bit | Son Ho | 1 | -5/+0 |
2023-06-04 | Make progress on primitivesScript | Son Ho | 1 | -166/+125 |
2023-06-04 | Make more progress on primitivesScript.sml | Son Ho | 1 | -148/+136 |
2023-06-04 | Use lower case in the names for the HOL4 backend | Son Ho | 1 | -403/+401 |
2023-06-04 | Make progress on primitivesScript.sml and experiment a bit | Son Ho | 1 | -81/+312 |
2023-06-04 | Organize a bit the HOL files | Son Ho | 1 | -74/+19 |
2023-06-04 | Add a Holmakefile | Son Ho | 1 | -0/+1667 |