src/HOL/Tools/Function/function_core.ML
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