sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-08-29	Updated snapshots for Isabelle 2018	Thomas Bauereiss

2018-08-28	Adapt theory imports for Isabelle 2018	Thomas Bauereiss
	Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
2018-07-09	Simplify treating of undefined_bool in Lem library	Thomas Bauereiss
	Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list.
2018-06-21	Follow Sail2 renaming in Isabelle library	Thomas Bauereiss

2018-05-18	Make named theorem collections of state monad more fine-grained	Thomas Bauereiss

2018-05-17	Merge branch 'cheri-mono' into sail2	Brian Campbell

2018-05-11	Add snapshot of generated Isabelle theories	Thomas Bauereiss
	Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
2018-05-04	Add back purely sequential Lem generation	Thomas Bauereiss
	The datatype package of HOL4 does not support the prompt monad, so this patch restores the option to generate a model that only uses the state monad. Also add a Makefile target cheri_sequential.lem in the cheri/ directory.
2018-04-24	Add some explanations to free monad documentation	Thomas Bauereiss

2018-04-20	Make building of Isabelle heap image optional	Thomas Bauereiss

2018-04-19	Fix minor typo.	Prashanth Mundkur

2018-04-19	more nuanced discussion of generating HOL4 and Coq	Peter Sewell

2018-04-18	Add generated PDF of documentation draft --- comments welcome	Thomas Bauereiss
	Placed in lib/isabelle/manual/document.pdf Also fixed a few typos.
2018-04-18	Add first draft of Isabelle library documentation	Thomas Bauereiss