src/HOL/Tools/Function/function_core.ML
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Sat, 15 May 2010 17:59:06 +0200 wenzelm incorporated further conversions and conversionals, after some minor tuning;
Wed, 21 Apr 2010 15:45:33 +0200 krauss tolerate eta-variants in f_graph.cases (from inductive package); added test case;
Sat, 02 Jan 2010 23:18:58 +0100 krauss new year's resolution: reindented code in function package
Fri, 11 Dec 2009 14:43:56 +0100 haftmann moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
Mon, 23 Nov 2009 15:05:59 +0100 krauss eliminated dead code and some unused bindings, reported by polyml
Thu, 19 Nov 2009 14:46:33 +0100 wenzelm adapted Local_Theory.define -- eliminated odd thm kind;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 19:57:46 +0100 wenzelm inductive: eliminated obsolete kind;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Fri, 30 Oct 2009 01:32:06 +0100 krauss less verbose inductive invocation
Fri, 30 Oct 2009 01:32:06 +0100 krauss tuned
Fri, 30 Oct 2009 01:32:06 +0100 krauss absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
Wed, 28 Oct 2009 16:25:27 +0100 wenzelm conceal internal bindings;
Fri, 23 Oct 2009 16:22:10 +0200 krauss function package: more standard names for structures and files
less more (0) tip