History log of /seL4-l4v-master/l4v/lib/sep_algebra/Extended_Separation_Algebra.thy
Revision Date Author Comments
# a424d55e 09-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX
# 8c683ce6 10-Feb-2019 Callum Bannister <callum.bannister@data61.csiro.au>

lib: Fixed guess_exI to filter out multiple matches, added guess_spec
# 436eae28 10-Jan-2019 Callum Bannister <callum.bannister@data61.csiro.au>

lib: automation for separation logic & folds
# 75148000 11-Sep-2018 Callum Bannister <callum.bannister@data61.csiro.au>

lib+sysinit: add extended separation algebra and forward reasoning tactics

Added Extended Separation Algebra, which contains septraction and
separating coimplication.
Added Sep_Forward which contains tactics for reasoning forwards in
separation logic, updated sep_cancel.
Updated SysInit proofs.