| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 18:14:06 +0100 |
wenzelm |
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 15:21:22 +0100 |
wenzelm |
clarified certify vs. sharing;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 22:32:10 +0100 |
wenzelm |
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:21:28 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 18:25:50 +0200 |
wenzelm |
clarified Type.the_decl;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:26:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 12:04:21 +0200 |
wenzelm |
simplified Sorts.class_error: plain Proof.context;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Thu, 30 Dec 2010 22:07:18 +0100 |
wenzelm |
uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 22:23:56 +0100 |
wenzelm |
extra checking of name bindings for classes, types, consts;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2010 17:21:07 +0100 |
paulson |
prevention of self-referential type environments
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 22:28:59 +0200 |
wenzelm |
Type_Infer.preterm: eliminated separate Constraint;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 20:47:47 +0200 |
wenzelm |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:55:45 +0200 |
wenzelm |
common Type.appl_error, which also covers explicit constraints;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:38:59 +0200 |
wenzelm |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:13:11 +0200 |
wenzelm |
more systematic naming of tsig operations;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 10:43:08 +0200 |
wenzelm |
export Type.minimize_sort;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:29:04 +0100 |
wenzelm |
aliases for class/type/const;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 14:35:02 +0100 |
wenzelm |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
|
file |
diff |
annotate
|