From b3f5dd5bac689bee9770081215bd0b1fe1071084 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 22 Jan 2018 20:56:07 +0000
Subject: Update Lem shallow embedding to Sail2

- Remove vector start indices
- Library refactoring:  Definitions in sail_operators.lem now use Bitvector
  type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes

TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.
---
 lib/isabelle/Makefile | 2 +-
 lib/isabelle/ROOT     | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index f340b81b..5ff58069 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,4 +1,4 @@
-THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy Sail_operators_mwords.thy State.thy Prompt.thy
+THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy State.thy Prompt.thy
 
 .PHONY: all heap-img clean
 
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index 7e90cdf0..2062b64b 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -5,7 +5,6 @@ session "Sail" = "LEM" +
     State
     Prompt
     Sail_operators
-    Sail_operators_mwords
 
 (*session "Sail" = "Sail_Base" +
   options [document = false]
-- 
cgit v1.2.3