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

isabelle2021-1: CamkesCdlRefine 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-01-14 17:35:58 +11:00 committed by Gerwin Klein
parent 84713327a5
commit 68bb97ef66
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
camkes/cdl-refine/Eval_CAMKES_CDL.thy
View File

@ -532,7 +532,7 @@ lemmas word_rel_simps_small =
word_less_alt word_le_def word_uint_eq_iff uint_0_eq uint_1
(* need bintrunc to reduce numerals mod word size *)
uint_bintrunc bintrunc_numeral_simps bintrunc_1_1
numeral_One BIT_bin_simps BIT_special_simps
numeral_One
(* evaluating word size for bintrunc -- yuck *)
len_num0 len_num1 len_bit0 len_bit1
arith_simps mult_1_right pred_numeral_simps numeral_plus_one