| Mon, 05 Jun 2006 21:54:26 +0200 |
wenzelm |
export read/cert_expr;
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:06 +0200 |
wenzelm |
activate Defines: fix frees;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:16 +0200 |
wenzelm |
replaced abbrevs by term_syntax, which is both simpler and more general;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:01 +0200 |
wenzelm |
use conjunction stuff from conjunction.ML;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:26 +0200 |
wenzelm |
abbrevs: support print mode;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2006 21:29:04 +0100 |
wenzelm |
interpret: Proof.assert_forward_or_chain;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2006 17:15:35 +0100 |
ballarin |
Tuned signature of Locale.add_locale(_i).
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 15:22:40 +0100 |
ballarin |
add_locale(_i) returns internal locale name.
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 09:57:25 +0100 |
ballarin |
Internal restructuring: local parameters.
|
file |
diff |
annotate
|
| Thu, 16 Mar 2006 20:19:25 +0100 |
ballarin |
New interface function parameters_of_expr.
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:11 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:18 +0100 |
wenzelm |
simplified TableFun.join;
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 17:17:53 +0100 |
wenzelm |
added abbreviations: activated by init, no expressions yet;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:45 +0100 |
wenzelm |
renamed gen_duplicates to duplicates;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:52 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Fri, 03 Feb 2006 11:47:57 +0100 |
haftmann |
refined signature of locale module
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 16:31:35 +0100 |
wenzelm |
Proof.refine_insert;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 12:54:08 +0100 |
wenzelm |
theorem(_in_locale): Element.statement, Obtain.statement;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 10:12:45 +0100 |
ballarin |
*_asms_of fixed.
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:29:49 +0100 |
wenzelm |
LocalDefs;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:12 +0100 |
wenzelm |
init: include view;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 16:05:23 +0100 |
ballarin |
Interface to access the specification of a named locale.
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:40 +0100 |
wenzelm |
turned abstract_term into ProofContext.abs_def;
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:31 +0100 |
wenzelm |
removed the_params;
|
file |
diff |
annotate
|
| Sun, 22 Jan 2006 18:45:59 +0100 |
wenzelm |
added the_params;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2006 21:55:15 +0100 |
wenzelm |
put_facts: do not pretend local thms were named;
|
file |
diff |
annotate
|