diff options
| author | Thomas Bauereiss | 2018-02-26 13:22:11 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-26 13:31:34 +0000 |
| commit | ee123e2876c4fa5ae000256caeb7eb810e8c05f8 (patch) | |
| tree | b00951146619539131ef511db727e19d685b8286 /src | |
| parent | 30ba876d4c465d9a6cf2eba4eb1ac4c3dbc7ed22 (diff) | |
Rename some Isabelle theories
The suffix _lemmas is more descriptive than _extras.
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 2 |
2 files changed, 2 insertions, 2 deletions
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 *) |