src/HOL/Partial_Function.thy
2016-12-22 haftmann 2016-12-22 proper logical constants
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-14 Andreas Lochbihler 2015-04-14 move lemma from AFP/Coinductive
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
2015-02-11 Andreas Lochbihler 2015-02-11 add lemmas about flat_ord
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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