| 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
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:15 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 23:27:58 +0100 |
wenzelm |
added init;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 10:28:31 +0100 |
haftmann |
fix: reintroduced pred_ctxt in gen_add_locale
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 11:32:16 +0100 |
haftmann |
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 00:06:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:53 +0100 |
wenzelm |
Logic.mk_conjunction_list;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:04 +0100 |
wenzelm |
CONJUNCTS2;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 13:25:20 +0100 |
haftmann |
discontinued unflat in favour of burrow and burrow_split
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 15:52:05 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
| Fri, 09 Dec 2005 09:06:45 +0100 |
haftmann |
oriented result pairs in PureThy
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 22:57:36 +0100 |
wenzelm |
defines: beta/eta contract lhs;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 08:06:59 +0100 |
haftmann |
introduced new map2, fold
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:22:28 +0100 |
wenzelm |
CONJUNCTS;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:36 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:52 +0100 |
wenzelm |
moved datatype elem to element.ML;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 10:43:15 +0100 |
wenzelm |
avoid prove_plain, export_plain, simplified after_qed;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:28:09 +0200 |
wenzelm |
tuned ProofContext.export interfaces;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:53 +0200 |
wenzelm |
Goal.prove_plain;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:34 +0200 |
wenzelm |
ObjectLogic.atomize_cterm;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:05 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 16:38:35 +0200 |
haftmann |
introduced AList module
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 12:18:05 +0200 |
wenzelm |
interpretation: use goal commands without target -- no storing of results;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 16:07:22 +0200 |
ballarin |
tuned
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 14:46:31 +0200 |
ballarin |
interpretation uses primitive goal interface
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:04:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:39 +0200 |
wenzelm |
load late, after proof.ML;
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 12:18:15 +0200 |
ballarin |
fixed printing of locales
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 08:30:43 +0200 |
haftmann |
introduced some new-style AList operations
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 08:14:35 +0200 |
haftmann |
introduced binding priority 1 for linear combinators etc.
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 09:50:58 +0200 |
ballarin |
print_locale omits facts by default
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2005 09:25:03 +0200 |
haftmann |
add_locale_context(_i) now exporting elements (still some refinements to be done)
|
file |
diff |
annotate
|
| Wed, 24 Aug 2005 12:05:48 +0200 |
ballarin |
Interpretation in locales: extended back end;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 11:17:44 +0200 |
wenzelm |
added add_locale_context(_i), which returns the body context for presentation;
|
file |
diff |
annotate
|