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

sys-init: Fix for Isabelle 2014.

This commit is contained in:
Andrew Boyton 2014-09-22 10:20:25 +10:00
parent 22b9118432
commit 57c57891bd
1 changed files with 1 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
sys-init/Proof_SI.thy
View File

@ -126,8 +126,7 @@ lemma capdl_objects_by_parts:
apply (subst (6) sep_map_set_conj_restrict [where t = "(\<lambda>obj. tcb_at obj spec)"], simp)
apply (subst (7) sep_map_set_conj_restrict [where t = "(\<lambda>obj. table_at obj spec)"], simp)
apply (subst (8) sep_map_set_conj_restrict [where t = "(\<lambda>obj. capless_at obj spec)"], simp)
apply (clarsimp simp: object_types_distinct real_cnode_at_def2 real_object_only_cnode
real_object_not_irq_node real_objects_some_type
apply (clarsimp simp: object_types_distinct real_object_not_irq_node real_objects_some_type
cong: rev_conj_cong)
done