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

word_lib: remove warning 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-02-25 10:48:47 +11:00
parent 83ddb4def9
commit ac1cda74f9
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Word_Lib/Word_Lib_Sumo.thy
View File

@ -134,6 +134,6 @@ lemmas cast_simps = cast_simps ucast_down_bl
lemma nth_ucast:
"(ucast (w::'a::len word)::'b::len word) !! n =
(w !! n \<and> n < min LENGTH('a) LENGTH('b))"
by (auto simp add: bit_simps not_le dest: bit_imp_le_length)
by (auto simp: not_le dest: bit_imp_le_length)
end