History log of /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/EXAMPLES/automatic/array_copy-shape.dsf
Revision Date Author Comments
# f8c63b1c 20-May-2010 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk>

- add multiple levels for expansions by holfoot-tactics, there were no_expands and do_expands, now there is full_expands as well. full_expands behaves like the old do_expands. do_expands does just fast expansions now
- fix a bug in the handling of assertions
- example array-inc added
- example quicksort-full-loopspec added


# dbcb3450 24-Mar-2010 Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk>

The shape of the quicksort example can be verified automatically now.
Array_copy example added.