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

trivial: remove a tab character 

tags: [NO_PROOF]
This commit is contained in:
Matthew Brecknell 2017-07-27 10:05:13 +10:00
parent 365643d751
commit 149ef38252
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/crefine/ARM/TcbQueue_C.thy
View File

@ -599,7 +599,7 @@ next
have nnull: "tn tcb \<noteq> NULL" using tq
proof (rule tcb_queue_relation_next_not_NULL)
from ind_prems show "\<forall>t\<in>set tcbs. tcb_at' t s"
and "distinct tcbs" by simp_all
and "distinct tcbs" by simp_all
show "tcbs \<noteq> []" using Cons by simp
qed