History log of /seL4-l4v-master/isabelle/src/HOL/SPARK/Manual/Proc2.thy
Revision Date Author Comments
# e60cf64d 06-Jan-2019 wenzelm <none@none>

isabelle update -u path_cartouches;


# 3347ed1a 03-Nov-2017 wenzelm <none@none>

less global theories -- avoid confusion about special cases;


# 17bc899d 18-Aug-2017 wenzelm <none@none>

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;


# c32926df 17-Dec-2016 haftmann <none@none>

reoriented congruence rules in non-explosive direction

--HG--
extra : rebase_source : 7b0d0d20a7c78db1ac5f12fb0d4ab0d915d0f2a3


# ceaee95a 01-Sep-2014 blanchet <none@none>

ported to use new-style datatypes
* * *
compile


# cb851030 30-Apr-2014 berghofe <none@none>

Discontinued old spark_open; spark_open_siv is now spark_open


# 42948201 22-Sep-2011 berghofe <none@none>

Added documentation for HOL-SPARK