sail/lib/isabelle/manual, branch sail2 Formal specification language for ISAs Updated snapshots for Isabelle 2018 2018-08-29T14:35:44+00:00 Thomas Bauereiss 2018-08-29T14:35:44+00:00 07e3591e2427db2d9407d554ac57984ca566c6ed 






Adapt theory imports for Isabelle 2018
2018-08-28T17:10:13+00:00

Thomas Bauereiss

2018-08-28T16:31:43+00:00

9232814ed220cff16e6cac808f327b326f2e2f2c

Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860





Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860







Simplify treating of undefined_bool in Lem library
2018-07-09T13:38:51+00:00

Thomas Bauereiss

2018-06-22T18:03:02+00:00

edc2be164fcf53c333796e55b93f94bf6c9ed152

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.





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.







Follow Sail2 renaming in Isabelle library
2018-06-21T16:54:17+00:00

Thomas Bauereiss

2018-06-21T16:50:54+00:00

2005eb7c190f8d28d6499df3dd77cf65a87e60cb












Make named theorem collections of state monad more fine-grained
2018-05-18T19:11:24+00:00

Thomas Bauereiss

2018-05-18T15:57:50+00:00

e2aa34b0ba28d89eab9f845fe904d4fdebb17395












Merge branch 'cheri-mono' into sail2
2018-05-17T15:39:30+00:00

Brian Campbell

2018-05-17T15:39:30+00:00

1867ec89a4493ca6ce92c8926885c4090b6d3d5d












Add snapshot of generated Isabelle theories
2018-05-11T15:11:51+00:00

Thomas Bauereiss

2018-05-11T14:25:27+00:00

3b2185dabdd5003c7553a7c86eab201cdebd5630

Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.





Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.







Add back purely sequential Lem generation
2018-05-04T19:29:19+00:00

Thomas Bauereiss

2018-05-04T19:29:19+00:00

f469001209e0333dbdd8fe42c7232c92a6c1be6f

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.





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.







Add some explanations to free monad documentation
2018-04-24T14:55:15+00:00

Thomas Bauereiss

2018-04-24T14:55:03+00:00

abfbc9bed6b533d2b4d95ef14ebc0063efae5d11












Make building of Isabelle heap image optional
2018-04-20T14:50:19+00:00

Thomas Bauereiss

2018-04-20T14:47:21+00:00

85d6051f04a5ffa93f35f3a6f4471aebfecd5c29