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

infoflow: update InfoFlowC session for Isabelle2020 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-10-21 16:30:28 +10:00 committed by Gerwin Klein
parent f0ffe07888
commit ad2e73ce4d
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/infoflow/refine/ADT_IF_Refine.thy
View File

@ -1227,7 +1227,7 @@ lemma handlePreemption_if_valid_domain_time:
"\<lbrace>\<top>\<rbrace>
handlePreemption_if tc
\<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace>"
unfolding handlePreemption_if_def by wpsimp
unfolding handlePreemption_if_def by (wpsimp cong: if_cong)
lemma schedule'_if_valid_domain_time:
"\<lbrace>\<top>\<rbrace> schedule'_if tc \<lbrace>\<lambda>_ s. 0 < ksDomainTime s\<rbrace>"