| Thu, 27 Sep 2007 17:57:12 +0200 |
wenzelm |
proper handling of chained facts;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 21:07:38 +0200 |
wenzelm |
eliminated ProofContext.read_termTs;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:27 +0200 |
wenzelm |
TypeInfer.constrain: canonical argument order;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:34 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:51 +0200 |
wenzelm |
Method.Basic: include position;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2007 20:44:08 +0200 |
wenzelm |
simplified ProofContext.read_termTs;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 10:01:43 +0200 |
ballarin |
Experimental interpretation code for definitions.
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:08 +0100 |
wenzelm |
moved parts of OuterParse to SpecParse;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:17 +0100 |
wenzelm |
Element.generalize_facts;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:52:23 +0100 |
wenzelm |
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:37 +0100 |
wenzelm |
notes: proper kind;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:22 +0200 |
wenzelm |
Element.export_facts;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:59 +0200 |
wenzelm |
simplified Proof.end_block;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 21:28:59 +0200 |
wenzelm |
proper Element.generalize_facts;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:38:01 +0200 |
wenzelm |
ProofContext.exports: simultaneous facts;
|
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 22:14:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 09:14:41 +0200 |
haftmann |
fixed smlnj incompat.
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:30 +0200 |
wenzelm |
actually invoke result elements;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:36 +0200 |
wenzelm |
Schematic invocation of locale expression in proof context.
|
file |
diff |
annotate
|