summaryrefslogtreecommitdiff
path: root/lib/isabelle
AgeCommit message (Expand)Author
2020-05-13Make Isabelle lemma generation work with grouped regstateThomas Bauereiss
2019-11-14Update location of sail2_instr_kinds.lemRobert Norton
2019-11-14Perform isabelle check only when heap-img rule is used to avoid calling opam ...Robert Norton
2019-05-08Remove generated TeX fileThomas Bauereiss
2019-05-07Patch up a couple of Isabelle proofs due to memory interface changesBrian Campbell
2019-04-25More read/write function updatesBrian Campbell
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-01-31Build Isabelle heap image instead of just running sessionThomas Bauereiss
2019-01-31Merge branch 'monads' into asl_flow2Thomas Bauereiss
2019-01-23Don't let "make" fail unnecessarily in lib/isabelleThomas Bauereiss
2019-01-21The RISCV environment variable collides with common usage by the RISC-V toolc...Prashanth Mundkur
2019-01-21Pass Lem library path to IsabelleThomas Bauereiss
2019-01-21Don't require manual set up of Isabelle session directoriesThomas Bauereiss
2019-01-21Fix build of Isabelle documentationThomas Bauereiss
2019-01-04Add a few helper lemmasThomas Bauereiss
2018-12-03Add Write_mem event/outcome without tagThomas Bauereiss
2018-12-03Make names of memory r/w events more consistentThomas Bauereiss
2018-11-30Rename Undefined outcome to ChooseThomas Bauereiss
2018-11-29Add separate outcome/event for tagged memory loadsThomas Bauereiss
2018-11-29Add some helper lemmas to Isabelle libThomas Bauereiss
2018-11-20Use nat instead of (list bitU) for addresses in monad outcomesThomas Bauereiss
2018-10-31Fix Isabelle libraryThomas Bauereiss
2018-08-29Updated snapshots for Isabelle 2018Thomas Bauereiss
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
2018-08-02Update a few prover gitignoresBrian Campbell
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix some signedness bugsThomas Bauereiss
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-09Update gitignoreThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Add lemmas about monadic Boolean connectivesThomas Bauereiss
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-11Add snapshot of generated Isabelle theoriesThomas Bauereiss
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-04-24Add some explanations to free monad documentationThomas Bauereiss
2018-04-20Make building of Isabelle heap image optionalThomas Bauereiss
2018-04-19Fix minor typo.Prashanth Mundkur
2018-04-19more nuanced discussion of generating HOL4 and CoqPeter Sewell
2018-04-18Add generated PDF of documentation draft --- comments welcomeThomas Bauereiss
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-18Add a simple Hoare logic for sequential reasoning to the libraryThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-04-13Add a few more generated file to gitignoreBrian Campbell
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:47:12 +0000