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