Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
Tue, 18 Jul 2006 20:01:46 +0200 |
wenzelm |
print_statement: tuned Variable operations;
|
file |
diff |
annotate
|
Tue, 11 Jul 2006 11:17:09 +0200 |
ballarin |
New function transfer_witness lifting Thm.transfer to witnesses.
|
file |
diff |
annotate
|
Sat, 08 Jul 2006 12:54:46 +0200 |
wenzelm |
prove_witness: context;
|
file |
diff |
annotate
|
Tue, 04 Jul 2006 19:49:58 +0200 |
wenzelm |
instantiate_tfrees: Thm.generalize;
|
file |
diff |
annotate
|
Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
Thu, 15 Jun 2006 23:08:54 +0200 |
wenzelm |
ProofContext: moved variable operations to struct Variable;
|
file |
diff |
annotate
|
Mon, 12 Jun 2006 21:19:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 11 Jun 2006 21:59:23 +0200 |
wenzelm |
added satisfy_ctxt;
|
file |
diff |
annotate
|
Wed, 07 Jun 2006 02:01:31 +0200 |
wenzelm |
added facts_of;
|
file |
diff |
annotate
|
Mon, 05 Jun 2006 21:54:23 +0200 |
wenzelm |
added params_of, prems_of;
|
file |
diff |
annotate
|
Fri, 26 May 2006 22:20:05 +0200 |
wenzelm |
pretty: do not exterm thm names;
|
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
|
Tue, 25 Apr 2006 22:23:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
Tue, 14 Mar 2006 22:06:36 +0100 |
wenzelm |
added pretty_statement;
|
file |
diff |
annotate
|
Tue, 14 Mar 2006 16:29:36 +0100 |
wenzelm |
added pretty_stmt;
|
file |
diff |
annotate
|
Thu, 02 Feb 2006 16:31:34 +0100 |
wenzelm |
always use Attrib.src;
|
file |
diff |
annotate
|
Thu, 02 Feb 2006 12:52:19 +0100 |
wenzelm |
added concluding statements: Shows/Obtains;
|
file |
diff |
annotate
|
Fri, 13 Jan 2006 01:13:08 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
Sat, 07 Jan 2006 12:26:31 +0100 |
wenzelm |
pretty_locale: backquote notes;
|
file |
diff |
annotate
|
Wed, 09 Nov 2005 16:26:55 +0100 |
wenzelm |
Explicit data structures for some Isar language elements.
|
file |
diff |
annotate
|