src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-18 wenzelm 2013-08-18 prefer plain subscript;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-02-25 wenzelm 2013-02-25 prefer stateless 'ML_val' for tests;
2011-10-10 bulwahn 2011-10-10 increasing values_timeout to avoid SML_makeall failures on our current tests
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2011-04-01 krauss 2011-04-01 raised timeouts further, for SML/NJ
2011-03-28 krauss 2011-03-28 raised various timeouts to accommodate sluggish SML/NJ
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-10-21 bulwahn 2010-10-21 adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-10-04 haftmann 2010-10-04 adjusted to inductive characterization of sorted
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-05-19 bulwahn 2010-05-19 adapting examples
2010-04-21 bulwahn 2010-04-21 adopting examples to changes in the predicate compiler
2010-03-31 bulwahn 2010-03-31 adopting specialisation examples to moving the alternative defs in the library
2010-03-29 bulwahn 2010-03-29 adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
2010-03-29 bulwahn 2010-03-29 adding specialisation examples of the predicate compiler