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