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

x64: crefine: adjust value_abbreviation in Delete_C

This commit is contained in:
Joel Beeren 2017-11-01 16:50:03 +11:00
parent fa38926ac3
commit 1079673d34
1 changed files with 0 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
proof/crefine/X64/Delete_C.thy
View File

@ -61,9 +61,6 @@ lemma ccorres_cutMon:
value_abbreviation zombie_magic "word_bits - cte_level_bits"
schematic_goal[simp]: "zombie_magic = ?P"
by ( simp add: cte_level_bits_def word_bits_def)
lemma unat_of_nat_zombie_magic[simp]: "unat ((of_nat zombie_magic) :: machine_word) = zombie_magic"
by (clarsimp simp: unat_of_nat64)