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
|
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
|