| 2014-03-13 |
wenzelm |
more frugal recording of changes: join merely requires information from one side;
|
file |
diff |
annotate
|
| 2014-03-11 |
wenzelm |
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
|
file |
diff |
annotate
|
| 2014-03-11 |
wenzelm |
minor performance tuning via fast matching filter;
|
file |
diff |
annotate
|
| 2014-03-10 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| 2014-03-09 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| 2014-03-06 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
| 2014-03-05 |
wenzelm |
more markup for inner syntax class/type names (notably for completion);
|
file |
diff |
annotate
|
| 2014-03-02 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
file |
diff |
annotate
|
| 2013-05-11 |
wenzelm |
prefer explicitly qualified exceptions, which is particular important for robust handlers;
|
file |
diff |
annotate
|
| 2013-04-12 |
wenzelm |
tuned exceptions -- avoid composing error messages in low-level situations;
|
file |
diff |
annotate
|
| 2012-11-25 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| 2012-10-03 |
wenzelm |
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
|
file |
diff |
annotate
|
| 2012-08-29 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| 2012-03-18 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| 2012-02-24 |
wenzelm |
clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
|
file |
diff |
annotate
|
| 2011-11-28 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| 2011-11-20 |
wenzelm |
clarified certify vs. sharing;
|
file |
diff |
annotate
|
| 2011-11-10 |
wenzelm |
pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
|
file |
diff |
annotate
|
| 2011-08-10 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| 2011-06-25 |
wenzelm |
entity markup for "type", "constant";
|
file |
diff |
annotate
|
| 2011-06-25 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
| 2011-06-09 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| 2011-06-09 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| 2011-04-23 |
wenzelm |
clarified Type.the_decl;
|
file |
diff |
annotate
|
| 2011-04-18 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| 2011-04-18 |
wenzelm |
simplified Sorts.class_error: plain Proof.context;
|
file |
diff |
annotate
|
| 2011-04-18 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| 2011-04-17 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| 2011-04-17 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| 2011-04-16 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| 2010-12-30 |
wenzelm |
uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
|
file |
diff |
annotate
|
| 2010-12-17 |
wenzelm |
extra checking of name bindings for classes, types, consts;
|
file |
diff |
annotate
|
| 2010-10-15 |
paulson |
prevention of self-referential type environments
|
file |
diff |
annotate
|
| 2010-09-12 |
wenzelm |
Type_Infer.preterm: eliminated separate Constraint;
|
file |
diff |
annotate
|
| 2010-09-12 |
wenzelm |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
|
file |
diff |
annotate
|
| 2010-09-12 |
wenzelm |
common Type.appl_error, which also covers explicit constraints;
|
file |
diff |
annotate
|
| 2010-09-12 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| 2010-05-04 |
wenzelm |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
|
file |
diff |
annotate
|
| 2010-04-28 |
wenzelm |
more systematic naming of tsig operations;
|
file |
diff |
annotate
|
| 2010-04-28 |
wenzelm |
export Type.minimize_sort;
|
file |
diff |
annotate
|
| 2010-03-20 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| 2010-03-09 |
wenzelm |
aliases for class/type/const;
|
file |
diff |
annotate
|
| 2010-03-09 |
wenzelm |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
|
file |
diff |
annotate
|
| 2010-02-25 |
wenzelm |
provide direct access to the different kinds of type declarations;
|
file |
diff |
annotate
|
| 2010-01-05 |
haftmann |
avoid exporting Type.build_tsig
|
file |
diff |
annotate
|
| 2009-12-02 |
haftmann |
exported build_tsig
|
file |
diff |
annotate
|
| 2009-11-21 |
wenzelm |
explicitly mark some legacy freeze operations;
|
file |
diff |
annotate
|
| 2009-11-09 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
file |
diff |
annotate
|
| 2009-11-08 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| 2009-10-25 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| 2009-10-24 |
wenzelm |
maintain position of formal entities via name space;
|
file |
diff |
annotate
|
| 2009-10-24 |
wenzelm |
maintain explicit name space kind;
|
file |
diff |
annotate
|
| 2009-10-24 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| 2009-10-24 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
| 2009-09-30 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| 2009-09-29 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 2009-09-23 |
paulson |
Correct chasing of type variable instantiations during type unification.
|
file |
diff |
annotate
|
| 2009-07-17 |
wenzelm |
eq_type: special case for empty environment;
|
file |
diff |
annotate
|
| 2009-07-06 |
wenzelm |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
file |
diff |
annotate
|
| 2009-03-07 |
wenzelm |
replace old bstring by binding for logical primitives: class, type, const etc.;
|
file |
diff |
annotate
|