summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-04-04Coq: improve solver on conjunctions, Euclidean division/moduloBrian Campbell
2019-03-27Coq: add a little knowledge about ZEuclid.divBrian Campbell
2019-03-27Coq: replace firstorder with less expensive tacticsBrian Campbell
2019-03-22Tidy up of div and mod operators (C implementation was previously inconsisten...Robert Norton
2019-03-19Coq: more test workBrian Campbell
2019-03-19Coq: more work on testsBrian Campbell
2019-03-18Add non-negative constraints for zeros/onesBrian Campbell
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-15Make mono_rewrites less dependant on ASL preludeThomas Bauereiss
2019-03-15Coq: some progress on the test suiteBrian Campbell
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-13C: Add missing update_lbits builtinAlasdair Armstrong
2019-03-12Coq: try non-linear nia solver tooBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
2019-03-08Fix the Coq mapping for eq_string in Sail lib.Prashanth Mundkur
2019-03-08Adds the DC and IC instructions to AArch64_small;Shaked Flur
2019-03-07Fix bug in a mono rewrite helper functionThomas Bauereiss
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
2019-03-05Coq 8.9 compatibility fixBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
2019-02-28Coq: more for informative booleansBrian Campbell
2019-02-28Coq: some work on bool simplificationBrian Campbell
2019-02-25Fix some builtins, and make mod_int return naturalAlasdair Armstrong
2019-02-21Allow monomorphisation with C generationAlasdair
2019-02-08Add missing functions to HOL monad wrapperThomas Bauereiss
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
2019-02-06Fix some testsAlasdair Armstrong
2019-02-06Remove all sizeof rewriting from C compilationAlasdair
2019-02-04Fix some warningsAlasdair Armstrong
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Tweak HOL LEM_DIR to match riscv makefileBrian Campbell
2019-02-01Make hol libraries use opam Lem library by defaultBrian Campbell
2019-01-31Build Isabelle heap image instead of just running sessionThomas Bauereiss
2019-01-31Adapt HOL library to monad changesThomas Bauereiss
2019-01-31Merge branch 'monads' into asl_flow2Thomas Bauereiss
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-23Don't let "make" fail unnecessarily in lib/isabelleThomas Bauereiss
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
2019-01-22Make sure we optimize constrained union constructorsAlasdair
2019-01-21The RISCV environment variable collides with common usage by the RISC-V toolc...Prashanth Mundkur
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:42:20 +0000