src/HOL/SPARK/SPARK_Setup.thy
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-07-11 wenzelm 2016-07-11 tuned;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2014-04-30 berghofe 2014-04-30 Discontinued old spark_open; spark_open_siv is now spark_open
2014-02-27 wenzelm 2014-02-27 modernized theory setup;
2013-11-13 haftmann 2013-11-13 separated comparision on bit operations into separate theory
2012-08-23 wenzelm 2012-08-23 added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-04-19 berghofe 2011-04-19 - renamed enum type class to spark_enum, to avoid confusion with enum type class defined in Enum theory - renamed theorem ..._card_UNIV to ..._card
2011-01-27 berghofe 2011-01-27 Tuned definition of sdiv.
2011-01-26 berghofe 2011-01-26 Replaced smod by standard mod operator to reflect actual behaviour of the SPARK tools.
2011-01-15 berghofe 2011-01-15 Added new SPARK verification environment.