From 3b2185dabdd5003c7553a7c86eab201cdebd5630 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 11 May 2018 15:25:27 +0100
Subject: Add snapshot of generated Isabelle theories

Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
---
 lib/isabelle/manual/Manual.thy   |   2 +-
 lib/isabelle/manual/document.pdf | Bin 216829 -> 0 bytes
 2 files changed, 1 insertion(+), 1 deletion(-)
 delete mode 100644 lib/isabelle/manual/document.pdf

(limited to 'lib')

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
deleted file mode 100644
index 200f8e22..00000000
Binary files a/lib/isabelle/manual/document.pdf and /dev/null differ
-- 
cgit v1.2.3