History log of /seL4-l4v-10.1.1/HOL4/src/bag/bagSyntax.sig
Revision Date Author Comments
# 271c8c35 16-Nov-2009 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk>

BAG_EVERY added to bagSyntax


# 8585ec8a 14-Oct-2009 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk>

Some more additions to bagLib. I'm mainly interested in bags that consists of multiple insertions into the empty bag like for example {|x1;x2;x3|}.
I call these explicitly given, finite bags "simple".

There was a lot of tool support for handling bags that consists of BAG_UNION applications. One can eliminate those for example on both sides of an equation, a BAG_DIFF ...
Now I added support for these "simple" bags. I started adding some things like resorting to bagLib before. However, these addidtion became larger and larger. Therefore, I moved them
into an new file called bagSimpleLib. However, it is imported by bagLib, so the end-user does not need to know this.


# 5086ec23 19-Sep-2009 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk>

BAG_IMAGE_CONV added that is able to evaluate BAG_IMAGE on very simple bags. Moreover, some extensions to bagSyntax were made.


# 59db6c3d 18-Jun-2001 Konrad Slind <konrad.slind@gmail.com>

Slight re-org.