diff options
| author | Thomas Bauereiss | 2018-07-11 00:14:57 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-11 00:21:19 +0100 |
| commit | 9bdd053dfca7c3e3ac6717a7d2b112ef17e20895 (patch) | |
| tree | 256a8c3625b1a2336379f652a84c82d894826b9f /snapshots/isabelle/lib/lem/Lem_machine_word.thy | |
| parent | 443fec23008a47eceb8ecb1ad5876e1d5d5e16af (diff) | |
Update Isabelle snapshots
Except RISC-V duopod, which doesn't seem to build for me at the moment
Diffstat (limited to 'snapshots/isabelle/lib/lem/Lem_machine_word.thy')
| -rw-r--r-- | snapshots/isabelle/lib/lem/Lem_machine_word.thy | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_machine_word.thy b/snapshots/isabelle/lib/lem/Lem_machine_word.thy index 3f83789c..85323bb2 100644 --- a/snapshots/isabelle/lib/lem/Lem_machine_word.thy +++ b/snapshots/isabelle/lib/lem/Lem_machine_word.thy @@ -8,13 +8,14 @@ imports "Lem_num" "Lem_basic_classes" "Lem_show" + "Lem_function" "~~/src/HOL/Word/Word" begin -(*open import Bool Num Basic_classes Show*) +(*open import Bool Num Basic_classes Show Function*) (*open import {isabelle} `~~/src/HOL/Word/Word`*) (*open import {hol} `wordsTheory` `wordsLib` `bitstringTheory` `integer_wordTheory`*) |