src/HOL/Tools/Function/partial_function.ML
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
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-18 wenzelm 2011-04-18 standardized aliases of operations on tsig;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-13 krauss 2010-12-13 eliminated dest_all_all_ctx
2010-10-26 haftmann 2010-10-26 partial_function is a declaration command
2010-10-26 krauss 2010-10-26 fixed confusion introduced in 008dc2d2c395
2010-10-26 krauss 2010-10-26 added Spec_Rule declaration to partial_function
2010-10-26 krauss 2010-10-26 declare recursive equation as ".simps", in accordance with other packages
2010-10-23 krauss 2010-10-23 first version of partial_function package