2014-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized module name and setup;
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2013-12-05 Andreas Lochbihler 2013-12-05 restrict admissibility to non-empty chains to allow more syntax-directed proof rules
2013-09-27 Andreas Lochbihler 2013-09-27 generalise lemma
2013-09-02 Andreas Lochbihler 2013-09-02 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
2013-07-24 krauss 2013-07-24 derive specialized version of full fixpoint induction (with admissibility)
2013-03-22 krauss 2013-03-22 added rudimentary induction rule for partial_function (heap)
2013-03-19 Andreas Lochbihler 2013-03-19 add induction rule for partial_function (tailrec)
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-12-29 huffman 2011-12-29 remove constant 'ccpo.lub', re-use constant 'Sup' instead
2011-10-29 wenzelm 2011-10-29 tuned;
2011-05-31 krauss 2011-05-31 generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
2011-05-31 krauss 2011-05-31 admissibility on option type
2011-05-23 krauss 2011-05-23 also manage induction rule; tuned data slot
2011-05-23 krauss 2011-05-23 separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
2010-10-29 krauss 2010-10-29 added rule let_mono
2010-10-29 krauss 2010-10-29 hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
2010-10-23 krauss 2010-10-23 first version of partial_function package