adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

word_lib: remove unused theories 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2021-01-22 09:41:38 +11:00 committed by Gerwin Klein
parent 8715767431
commit 4afa4734a5
3 changed files with 1 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
lib/Word_Lib/Word_Setup_32.thy
View File

@ -1,16 +0,0 @@
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
section "32-Bit Machine Word Setup"
theory Word_Setup_32
imports "HOL-Library.Word"
begin
text \<open>This theory defines standard platform-specific word size and alignment.\<close>
end

15
lib/Word_Lib/Word_Setup_64.thy
View File

@ -1,15 +0,0 @@
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
section "64-Bit Machine Word Setup"
theory Word_Setup_64
imports "HOL-Library.Word"
begin
text \<open>This theory defines standard platform-specific word size and alignment.\<close>
end

2
proof/sep-capDL/Separation_SD.thy
View File

@ -296,7 +296,7 @@ lemma offset_slot':
"\<lbrakk>slot < 2^radix\<rbrakk> \<Longrightarrow> offset slot radix = unat slot"
by (clarsimp simp: offset_def Word.less_mask_eq)
lemmas word_bits_def = Word_Setup_32.word_bits_def
lemmas word_bits_def = Word_32.word_bits_def
lemma offset_slot:
"\<lbrakk>slot < 2^radix; radix < word_bits\<rbrakk> \<Longrightarrow> offset (of_nat slot) radix = slot"