diff options
Diffstat (limited to 'lib/isabelle/Sail2_state_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Sail2_state_monad_lemmas.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index 1e9f50cc..2fbd7a56 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -214,11 +214,11 @@ lemma no_throw_mem_builtins: "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s" "\<And>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" - "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s" + "\<And>BCa BCv rk asz a sz s. ignore_throw (read_memS BCa BCv rk asz a sz) s = read_memS BCa BCv rk asz a sz s" "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s" "\<And>BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s" "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s" - "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s" + "\<And>BCa BCv wk asz addr sz v s. ignore_throw (write_memS BCa BCv wk asz addr sz v) s = write_memS BCa BCv wk asz addr sz v s" "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS BCa BCv wk addr sz v t s" "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" |