| Mon, 29 Sep 2008 21:45:44 +0200 |
wenzelm |
put_thms: ContextPosition.set_visible false;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 21:26:36 +0200 |
wenzelm |
back to plain Position.report for regular references;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 14:41:25 +0200 |
wenzelm |
ContextPosition.report;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 10:58:04 +0200 |
wenzelm |
added norm_export_morphism;
|
file |
diff |
annotate
|
| Fri, 12 Sep 2008 12:04:20 +0200 |
wenzelm |
added extern_fact (local or global);
|
file |
diff |
annotate
|
| Fri, 12 Sep 2008 10:54:00 +0200 |
wenzelm |
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 18:01:24 +0200 |
wenzelm |
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:32 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:52 +0200 |
wenzelm |
retrieve_thms: transfer fact position to result;
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 18:37:49 +0200 |
wenzelm |
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
|
file |
diff |
annotate
|
| Sun, 10 Aug 2008 12:38:25 +0200 |
wenzelm |
read_tyname/const/const_proper: report position;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 22:32:01 +0200 |
wenzelm |
parse_token: use Syntax.read_token, pass full position information;
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 00:12:02 +0200 |
wenzelm |
parse_sort/typ/term/prop: report markup;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 13:31:31 +0200 |
wenzelm |
Facts.lookup: return static/dynamic status;
|
file |
diff |
annotate
|
| Sat, 21 Jun 2008 16:18:51 +0200 |
wenzelm |
added query_type/const/class (meta data);
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 22:05:05 +0200 |
wenzelm |
renamed is_abbrev_mode to abbrev_mode;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 22:32:03 +0200 |
wenzelm |
simplified TypeInfer.infer_types;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:07 +0200 |
wenzelm |
export transfer_syntax;
|
file |
diff |
annotate
|
| Fri, 13 Jun 2008 21:04:42 +0200 |
wenzelm |
map_const: soft version, no failure here;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 16:41:47 +0200 |
wenzelm |
Facts.dest/export_static: content difference;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:26 +0200 |
wenzelm |
unparse_term: check PureThy.old_appl_syntax instead of CPure;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 14:27:02 +0200 |
wenzelm |
default token translations: observe Sign.is_pretty_global for fixed variables;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:13 +0200 |
haftmann |
exported is_abbrev mode discriminator
|
file |
diff |
annotate
|
| Fri, 18 Apr 2008 23:49:46 +0200 |
wenzelm |
print_cases: proper context for revert_skolem;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:30 +0200 |
wenzelm |
revert_skolem: do not change non-reversible names;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:51 +0200 |
wenzelm |
default token translations with proper markup;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 21:53:03 +0200 |
wenzelm |
Facts.extern_static;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 17:40:43 +0200 |
wenzelm |
removed obsolete valid_thms;
|
file |
diff |
annotate
|