src/Tools/induct.ML
Fri, 02 Oct 2009 22:15:08 +0200 wenzelm eliminated dead code;
Fri, 28 Aug 2009 21:04:03 +0200 wenzelm modernized messages -- eliminated ctyp/cterm operations;
Sat, 25 Jul 2009 12:43:45 +0200 wenzelm eliminated redundant Library.multiply;
Fri, 24 Jul 2009 12:33:00 +0200 wenzelm renamed functor InductFun to Induct;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Fri, 17 Jul 2009 21:33:00 +0200 wenzelm tuned/modernized Envir operations;
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Tue, 17 Mar 2009 14:12:43 +0100 wenzelm adapted to general Item_Net;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Tue, 03 Mar 2009 14:07:43 +0100 wenzelm Thm.binding;
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Thu, 26 Jun 2008 15:06:25 +0200 wenzelm Args.context;
Mon, 23 Jun 2008 15:26:53 +0200 wenzelm tuned get_inductT: *all* rules for missing instantiation;
Tue, 10 Jun 2008 23:28:42 +0200 wenzelm added del attributes;
Sun, 18 May 2008 15:04:17 +0200 wenzelm guess_instance: proper context;
Fri, 16 May 2008 21:53:30 +0200 wenzelm removed obsolete option open;
Thu, 17 Apr 2008 22:22:23 +0200 wenzelm adapted to ProofContext.revert_skolem: extra Name.clean required;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Mon, 07 Apr 2008 21:25:18 +0200 wenzelm renamed iterated forall_conv to params_conv;
Sat, 15 Mar 2008 22:07:32 +0100 wenzelm tuned messages;
Sat, 26 Jan 2008 20:01:37 +0100 wenzelm avoid redundant escaping of Isabelle symbols;
Thu, 24 Jan 2008 23:51:20 +0100 wenzelm replaced ContextPosition by Position.thread_data;
Fri, 19 Oct 2007 23:21:13 +0200 wenzelm warn_open: context position;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Fri, 05 Oct 2007 23:04:17 +0200 wenzelm (co)induct: polymorhic taking'';
Fri, 05 Oct 2007 22:00:15 +0200 wenzelm tuned Induct interface: prefer pred'' over set'';
Thu, 04 Oct 2007 16:59:28 +0200 wenzelm Conv.forall_conv: proper context;
Thu, 04 Oct 2007 14:42:47 +0200 wenzelm moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
less more (0) tip