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

c-parser: keep word_neq_0_conv[simp] for now

This commit is contained in:
Gerwin Klein 2019-06-05 11:15:16 +10:00 committed by Matthew Brecknell
parent 2e6bf613e2
commit 22433afbb7
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/c-parser/CTranslation.thy
View File

@ -183,4 +183,6 @@ lemma proc_deps_lvar_nondet_init [simp]:
"proc_deps (lvar_nondet_init accessor upd) \<Gamma> = {}"
by (simp add: lvar_nondet_init_def)
declare word_neq_0_conv[simp] (* FIXME: for backward compatibility; remove *)
end