rationalized internals

life without 'metis'

rationalized internals

rationalized internals

rationalize internals

optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant

compile

make 'diff_iff' a simp rule if available

less aggressive resolving

repaired argument list to corecursor

adapted to absence of 'unfold'

got rid of automatically generated fold constant and theorems (to reduce overhead)

use same identity function for abs and rep (doesn't seem to confuse any proofs)

make 'typedef' optional, depending on size of original type

use aconv to compare terms (for cleanliness)

tuning

optimize cardinal bounds involving natLeq (omega)

no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');

merged

more standard module name;

silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;

tuned whitespace;

allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;

tuned proofs;

prefer Name_Space.check with its builtin reports (including completion);

tuned source structure;

prefer Name_Space.check with its builtin reports (including completion);

consider completion report as part of error message -- less stateful, may get handled;

more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;

more antiquotations;

clarified names of antiquotations and markup; more documentation;

tuned proof

merged

tuned proofs

repaired document;

repaired document;

more markup for ML source;

merged

tuned signature;

clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";

clarified module structure;

tuned;

tuned signature -- separate module Font_Info;

tuned;

font size change with delay, to avoid GUI lagging behind user input;

incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;

more symbols, less parentheses;

tuned signature -- more explicit Document.Elements;

made SML/NJ happier

more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy

earlier setup of transfer, without dependency on psychodelic interpretations

cursory polishing: tuned proofs, tuned symbols, tuned headings

merged

tuned whitespace; more symbols;

allow completion within a word (or symbol), like semantic completion; no special treatment for History_Text_Field, due to lack of active range rendering;

more regular buffer_range, despite 47e8c8daccae; more robust invalidate_range, which is relevant when editing at the end of the buffer (NB: last line offset by be outside actual buffer length);

load Metis a little later

made SML/NJ happier

merged

added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets