src/HOL/Tools/Function/function_core.ML
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2009-12-11 haftmann 2009-12-11 moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-11-23 krauss 2009-11-23 eliminated dead code and some unused bindings, reported by polyml
2009-11-19 wenzelm 2009-11-19 adapted Local_Theory.define -- eliminated odd thm kind;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-10-30 krauss 2009-10-30 less verbose inductive invocation
2009-10-30 krauss 2009-10-30 tuned
2009-10-30 krauss 2009-10-30 absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files