rationalized internals

rationalized internals

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

added function "List.extract"

explicit link to Z3 license;

recovered minimal README from 30de372ca56f;

adapt examples to new intermediate typedef

joint work with blanchet: intermediate typedef for the input to fp-operations

prefer abstract datatype -- in accordance to ML version;

tuned data structure;

tuned;

tuned comment;

tuned signature;

tuned errors -- in accordance to Scala version;

tuned errors -- in accordance to ML antiquotations;

more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);

merged

tuned whitespace; tuned proofs;

tuned whitespace; modernized theory setup;

clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits; clarified asynchronous event propagation: determine buffers where they are actually accessed; tuned signature;

simplified rendering -- no need to over-emphasize "token_range";

modernized theory setup;

store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;

more symbols;

more symbol abbrevs to support HOL library maintenance;

reparse only for actually changed blobs; tuned signature;

proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;

more formal Document.Blobs; removed junk;

tuned output;

proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);

tuned iterator;

tuned;

tuned comment;

tuned output;

amended some slips, rolling back currently dysfunctional export minimimalisation for Scala

A bit of tidying up

added two examples