src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-03-01 ago more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2011-12-24 ago adjusted to set/pred distinction by means of type constructor `set`
2011-09-14 ago renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 ago new fastforce replacing fastsimp - less confusing name
2011-04-23 ago modernized specifications;
2011-04-04 ago raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
2011-03-28 ago raised various timeouts to accommodate sluggish SML/NJ
2010-12-29 ago explicit file specifications -- avoid secondary load path;
2010-12-02 ago adapted expected value to more idiomatic numeral representation
2010-10-25 ago changing test parameters in examples to get to a result within the global timelimit
2010-10-22 ago updating to new notation in commented examples
2010-09-30 ago adding example for case expressions
2010-09-29 ago added test case for predicate arguments in higher-order argument position
2010-09-29 ago added a test case to Predicate_Compile_Tests
2010-09-28 ago adding test case for interpretation of arguments that are predicates simply as input
2010-09-28 ago handling higher-order relations in output terms; improving proof procedure; added test case
2010-09-23 ago moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
2010-09-23 ago splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests