From ee123e2876c4fa5ae000256caeb7eb810e8c05f8 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 26 Feb 2018 13:22:11 +0000
Subject: Rename some Isabelle theories

The suffix _lemmas is more descriptive than _extras.
---
 src/gen_lib/prompt.lem | 2 +-
 src/gen_lib/state.lem  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 728014eb..bca09aa1 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,7 +2,7 @@ open import Pervasives_extra
 (*open import Sail_impl_base*)
 open import Sail_values
 open import Prompt_monad
-open import {isabelle} `Prompt_monad_extras`
+open import {isabelle} `Prompt_monad_lemmas`
 
 val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let rec iter_aux i f xs = match xs with
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 1740174e..1366e605 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -4,7 +4,7 @@ open import Sail_values
 open import Prompt_monad
 open import Prompt
 open import State_monad
-open import {isabelle} `State_monad_extras`
+open import {isabelle} `State_monad_lemmas`
 
 (* State monad wrapper around prompt monad *)
 
-- 
cgit v1.2.3