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

Word_Lib: make word_and_max_simps 64bit clean 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-09-23 14:32:41 +10:00 committed by Gerwin Klein
parent 414eb5ce3d
commit ac325266b8
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/Word_Lib/Word_Lemmas_64_Internal.thy
View File

@ -8,6 +8,9 @@ theory Word_Lemmas_64_Internal
imports Word_Lib_Sumo Word_64
begin
(* This is why Word_Lib_Sumo doesn't really work: *)
lemmas word_and_max_simps = word_and_max_simps word64_and_max_simp
lemmas unat_add_simple = iffD1[OF unat_add_lem[where 'a = 64, folded word_bits_def]]
lemma unat_length_4_helper: