summaryrefslogtreecommitdiff
path: root/lib/isabelle
AgeCommit message (Expand)Author
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
2018-03-05Add Print outcome to prompt monad for debugging and tracingThomas Bauereiss
2018-03-05Add support for undefined bit oracle to Lem shallow embeddingThomas Bauereiss
2018-02-26Rename some Isabelle theoriesThomas Bauereiss
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-01-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
2018-01-31Split base definitions of Lem monads and further built-ins (e.g. loop combina...Thomas Bauereiss
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2017-09-29Move Isabelle libraryThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:56:19 +0000