src/Pure/Isar/find_theorems.ML
Fri, 04 Jul 2008 16:33:08 +0200 huffman prefer theorem names without numbers
Thu, 12 Jun 2008 16:41:47 +0200 wenzelm Facts.dest/export_static: content difference;
Wed, 16 Apr 2008 21:52:58 +0200 wenzelm Facts.dest_static;
Tue, 15 Apr 2008 18:49:25 +0200 wenzelm Facts.dest_table, PureThy.facts_of;
Thu, 20 Mar 2008 16:04:30 +0100 wenzelm Facts.Named: include position;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Sat, 15 Mar 2008 18:08:03 +0100 wenzelm more precise Author line;
Sun, 27 Jan 2008 22:21:34 +0100 wenzelm renamed thms_containing_limit to FindTheorems.limit;
Mon, 29 Oct 2007 16:13:46 +0100 wenzelm improved notion of 'nicer' fact names (observe some name space properties);
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sun, 23 Sep 2007 22:23:34 +0200 wenzelm ProofContext.read_term_pattern;
Sun, 15 Apr 2007 23:25:50 +0200 wenzelm removed obsolete TypeInfer.logicT -- use dummyT;
Tue, 06 Mar 2007 05:09:53 +0100 kleing an O(n log n) version of removing duplicates
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
Wed, 21 Feb 2007 02:30:06 +0100 kleing prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)
Tue, 20 Feb 2007 00:14:33 +0100 kleing Remove duplicates from printed theorems in find_theorems
Sat, 29 Apr 2006 23:16:43 +0200 wenzelm tuned;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Wed, 26 Apr 2006 22:40:46 +0200 wenzelm *** empty log message ***
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct;
Mon, 06 Feb 2006 20:59:06 +0100 wenzelm tuned;
Thu, 01 Dec 2005 22:03:04 +0100 wenzelm ProofContext.lthms_containing: suppress obvious duplicates;
Wed, 16 Nov 2005 17:45:30 +0100 wenzelm tuned Pattern.match/unify;
Fri, 21 Oct 2005 18:14:52 +0200 wenzelm do not export find_thms;
Fri, 07 Oct 2005 23:29:00 +0200 wenzelm removed obsolete comment;
Tue, 04 Oct 2005 19:01:37 +0200 wenzelm minor tweaks for Poplog/ML;
Tue, 04 Oct 2005 16:47:40 +0200 wenzelm find_theorems: support * wildcard in name: criterion;
Wed, 31 Aug 2005 15:46:44 +0200 wenzelm refer to theory instead of low-level tsig;
Thu, 18 Aug 2005 11:17:41 +0200 wenzelm use theory instead of obsolete Sign.sg;
Mon, 01 Aug 2005 03:27:31 +0200 kleing Ordering is now: first by number of assumptions, second by the substitution size.
Wed, 20 Jul 2005 07:40:23 +0200 kleing Sort search results in order of relevance, where relevance =
Mon, 20 Jun 2005 22:13:59 +0200 wenzelm get_thm(s): Name;
Thu, 26 May 2005 10:05:28 +0200 kleing cleaned up select_match
Wed, 25 May 2005 11:18:02 +0200 kleing more cleanup
Wed, 25 May 2005 10:43:15 +0200 kleing renamed search criterion 'rewrite' to 'simp'
Wed, 25 May 2005 10:18:09 +0200 kleing removed obsolete findI, findE, findEs
Sun, 22 May 2005 19:26:16 +0200 wenzelm added read_criterion/pretty_criterion;
Sun, 22 May 2005 16:54:09 +0200 wenzelm Retrieve theorems from proof context -- improved version of
less more (0) tip