| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 17:17:47 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2005 16:04:54 +0200 |
wenzelm |
added (use_)legacy_bindings;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2005 19:51:54 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Mon, 26 Apr 2004 15:01:05 +0200 |
wenzelm |
use Syntax.is_ascii_identifier;
|
file |
diff |
annotate
|
| Tue, 02 Jul 2002 15:45:55 +0200 |
wenzelm |
removed thms_containing (see pure_thy.ML and proof_context.ML);
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:04:26 +0200 |
wenzelm |
moved goal related stuff to goals.ML;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:07:01 +0200 |
wenzelm |
added qed_spec_mp etc.;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:24:39 +0200 |
berghofe |
Exported ml_reserved.
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:43:14 +0100 |
wenzelm |
thms_containing: term args;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:35:50 +0100 |
wenzelm |
use_text etc.: proper output of error messages;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2001 20:04:41 +0100 |
wenzelm |
use_text_verbose: priority output;
|
file |
diff |
annotate
|
| Tue, 07 Dec 1999 11:01:48 +0100 |
nipkow |
Fixed bug in find-functions: list of parameters must be reversed before
|
file |
diff |
annotate
|
| Wed, 13 Oct 1999 19:42:12 +0200 |
wenzelm |
use_text_verbose;
|
file |
diff |
annotate
|
| Tue, 05 Oct 1999 16:55:13 +0200 |
wenzelm |
fixed ml_store_thm(s): deriv;
|
file |
diff |
annotate
|
| Sun, 26 Sep 1999 16:38:21 +0200 |
wenzelm |
added print_thms_containing;
|
file |
diff |
annotate
|
| Wed, 22 Sep 1999 20:58:23 +0200 |
wenzelm |
ml_store_thm: no warning for "";
|
file |
diff |
annotate
|
| Fri, 03 Sep 1999 13:55:46 +0200 |
wenzelm |
added no_qed;
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:09:10 +0200 |
wenzelm |
added store/bind_thms;
|
file |
diff |
annotate
|
| 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
|