diff options
| author | Thomas Bauereiss | 2018-05-11 15:25:27 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-11 16:11:51 +0100 |
| commit | 3b2185dabdd5003c7553a7c86eab201cdebd5630 (patch) | |
| tree | bda80e8df99789ac8594f92c571476d5a1b6db8e /lib | |
| parent | 2a6e5eca7b28c5069e402a34ec36b7a6e18b274e (diff) | |
Add snapshot of generated Isabelle theories
Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/manual/Manual.thy | 2 | ||||
| -rw-r--r-- | lib/isabelle/manual/document.pdf | bin | 216829 -> 0 bytes |
2 files changed, 1 insertions, 1 deletions
diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 53175ec9..6cdfbfa1 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -24,7 +24,7 @@ follow the instructions. In order to generate theorem prover definitions, Sail specifications are first translated to Lem, which then generates definitions for Isabelle/HOL. Lem can also generate HOL4 definitions, though we have -not yet tested that for our ISA specifications. To produce Coq +not yet tested that extensively for our ISA specifications. To produce Coq definitions, we envisage implementing a direct Sail-to-Coq backend, to preserve the Sail dependent types (it's possible that the Lem-to-Coq backend, which in general does not produce good Coq definitions, would diff --git a/lib/isabelle/manual/document.pdf b/lib/isabelle/manual/document.pdf Binary files differdeleted file mode 100644 index 200f8e22..00000000 --- a/lib/isabelle/manual/document.pdf +++ /dev/null |