index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
backends
/
hol4
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Use lower case in the names for the HOL4 backend
Son Ho
2023-06-04
5
-832
/
+771
*
Make progress on primitivesScript.sml and experiment a bit
Son Ho
2023-06-04
4
-87
/
+890
*
Make progress on the primitives library for HOL4
Son Ho
2023-06-04
3
-12
/
+196
*
Organize a bit the HOL files
Son Ho
2023-06-04
8
-190
/
+1160
*
Make minor modifications
Son Ho
2023-06-04
1
-5
/
+0
*
Add a Holmakefile
Son Ho
2023-06-04
5
-17
/
+2527
*
Make good progress on Primitives.sml
Son Ho
2023-06-04
1
-24
/
+997
*
Start working on Primitives.sml
Son Ho
2023-06-04
2
-5
/
+387
*
Add a more interesting example
Son Ho
2023-06-04
1
-1
/
+69
*
Implement a progress tactic
Son Ho
2023-06-04
1
-33
/
+339
*
Make more progress on the automation
Son Ho
2023-06-04
1
-51
/
+199
*
Make minor modifications to the HOL experiment
Son Ho
2023-06-04
1
-5
/
+25
*
Make progress on implementing tactics
Son Ho
2023-06-04
1
-27
/
+347
*
Implement [assume_bounds_for_all_int_vars] to improve the proof experience
Son Ho
2023-06-04
1
-80
/
+145
*
Start making tests in HOL4
Son Ho
2023-06-04
1
-0
/
+825