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.