| Fri, 06 Aug 1999 11:07:25 +0200 |
paulson |
now catches exn THEORY and prints an error message
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:17:40 +0100 |
wenzelm |
Present.theorem;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 17:23:35 +0100 |
wenzelm |
open BasicThmDatabase;
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 16:44:50 +0200 |
wenzelm |
export is_ml_identifier;
|
file |
diff |
annotate
|
| Thu, 20 Aug 1998 09:25:59 +0200 |
paulson |
Now qed_spec_mp respects locales, by calling ml_store_thm
|
file |
diff |
annotate
|
| Fri, 17 Jul 1998 10:50:28 +0200 |
paulson |
added comments
|
file |
diff |
annotate
|
| Mon, 29 Jun 1998 10:32:06 +0200 |
wenzelm |
use_text: verbose flag;
|
file |
diff |
annotate
|
| Mon, 15 Jun 1998 11:06:00 +0200 |
wenzelm |
use_text replaces use_strings;
|
file |
diff |
annotate
|
| Fri, 09 Jan 1998 14:02:34 +0100 |
wenzelm |
thm_ord;
|
file |
diff |
annotate
|
| Thu, 08 Jan 1998 18:19:48 +0100 |
wenzelm |
fixed thm_less;
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 09:58:03 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 16:37:43 +0100 |
wenzelm |
fixed type of thms_containing;
|
file |
diff |
annotate
|
| Thu, 30 Oct 1997 10:01:46 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Oct 1997 17:37:46 +0100 |
wenzelm |
restructured -- uses PureThy storage facilities;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:19:14 +0200 |
wenzelm |
ProtoPure.flexpair_def;
|
file |
diff |
annotate
|
| Thu, 23 Oct 1997 12:43:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 14:42:44 +0200 |
wenzelm |
renamed use_string to use_strings;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 14:12:03 +0200 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 00:18:34 +0200 |
berghofe |
Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
|
file |
diff |
annotate
|
| Fri, 01 Nov 1996 15:41:09 +0100 |
paulson |
Replaced "sum" (only usage?) by foldl op+
|
file |
diff |
annotate
|
| Fri, 17 May 1996 16:22:23 +0200 |
nipkow |
Added missing default clause | top_const _ = None;
|
file |
diff |
annotate
|
| Tue, 09 Apr 1996 12:12:27 +0200 |
berghofe |
select_match now sorts list of matching theorems according to the
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 12:01:19 +0100 |
berghofe |
Added some functions which allow redirection of Isabelle's output
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Wed, 25 Oct 1995 13:41:45 +0100 |
clasohm |
removed "duplicate" warning from store_thm_db;
|
file |
diff |
annotate
|
| Fri, 06 Oct 1995 14:43:26 +0100 |
clasohm |
changed some comments
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 12:59:52 +0100 |
clasohm |
added removal of theorems if theory is to be reloaded; changed functions for
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 14:25:52 +0200 |
clasohm |
fixed bug: duplicate "duplicate" warnings
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:28:54 +0200 |
clasohm |
added cleanup of global simpset to thy_read;
|
file |
diff |
annotate
|
| Wed, 30 Aug 1995 14:04:39 +0200 |
clasohm |
added check for duplicate theorems in theorem database;
|
file |
diff |
annotate
|
| Fri, 18 Aug 1995 12:28:02 +0200 |
nipkow |
fixed bug in findI
|
file |
diff |
annotate
|
| Mon, 07 Aug 1995 15:23:59 +0200 |
nipkow |
Added findI, findEs, and findE.
|
file |
diff |
annotate
|
| Thu, 01 Jun 1995 13:25:06 +0200 |
clasohm |
commented thms_unifying_with out; placed thm_db into signature again;
|
file |
diff |
annotate
|
| Tue, 30 May 1995 11:57:27 +0200 |
clasohm |
removed thm_num and thm_db from signature
|
file |
diff |
annotate
|
| Tue, 30 May 1995 11:28:13 +0200 |
clasohm |
fixed bug in thms_containing; changed error/warning messages;
|
file |
diff |
annotate
|
| Mon, 29 May 1995 15:04:27 +0200 |
clasohm |
changed error message in thms_containing
|
file |
diff |
annotate
|
| Mon, 29 May 1995 13:55:06 +0200 |
clasohm |
added theorem database which contains axioms and theorems indexed by the
|
file |
diff |
annotate
|