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