src/HOL/Partial_Function.thy
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