2014-02-28 traytel 2014-02-28 made SML/NJ happier
2014-02-28 nipkow 2014-02-28 merged
2014-02-28 nipkow 2014-02-28 added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
2014-02-28 nipkow 2014-02-28 added function "List.extract"
2014-02-28 wenzelm 2014-02-28 explicit link to Z3 license;
2014-02-28 wenzelm 2014-02-28 recovered minimal README from 30de372ca56f;
2014-02-27 traytel 2014-02-27 adapt examples to new intermediate typedef
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-28 wenzelm 2014-02-28 prefer abstract datatype -- in accordance to ML version;
2014-02-28 wenzelm 2014-02-28 tuned data structure;
2014-02-28 wenzelm 2014-02-28 tuned;
2014-02-28 wenzelm 2014-02-28 tuned comment;
2014-02-28 wenzelm 2014-02-28 tuned signature;
2014-02-28 wenzelm 2014-02-28 tuned errors -- in accordance to Scala version;
2014-02-28 wenzelm 2014-02-28 tuned errors -- in accordance to ML antiquotations;
2014-02-28 wenzelm 2014-02-28 more explicit method reports; avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);
2014-02-27 wenzelm 2014-02-27 merged
2014-02-27 wenzelm 2014-02-27 tuned whitespace; tuned proofs;
2014-02-27 wenzelm 2014-02-27 tuned whitespace; modernized theory setup;
2014-02-27 wenzelm 2014-02-27 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;
2014-02-27 wenzelm 2014-02-27 simplified rendering -- no need to over-emphasize "token_range";
2014-02-27 wenzelm 2014-02-27 modernized theory setup;
2014-02-27 wenzelm 2014-02-27 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;
2014-02-27 wenzelm 2014-02-27 more symbols;
2014-02-27 wenzelm 2014-02-27 more symbol abbrevs to support HOL library maintenance;
2014-02-27 wenzelm 2014-02-27 reparse only for actually changed blobs; tuned signature;
2014-02-27 wenzelm 2014-02-27 proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;
2014-02-27 wenzelm 2014-02-27 more formal Document.Blobs; removed junk;
2014-02-27 wenzelm 2014-02-27 tuned output;
2014-02-27 wenzelm 2014-02-27 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);
2014-02-27 wenzelm 2014-02-27 tuned iterator;
2014-02-27 wenzelm 2014-02-27 tuned;
2014-02-27 wenzelm 2014-02-27 tuned comment;
2014-02-26 wenzelm 2014-02-26 tuned output;
2014-02-27 haftmann 2014-02-27 amended some slips, rolling back currently dysfunctional export minimimalisation for Scala
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-02-27 blanchet 2014-02-27 added two examples
2014-02-27 kuncar 2014-02-27 hide Lifting.invariant from a user completely
2014-02-27 blanchet 2014-02-27 correct most general type for mutual recursion when several identical types are involved
2014-02-27 Lars Hupel 2014-02-27 removed bogus "error" message (it appeared during regular mode of operation)
2014-02-26 traytel 2014-02-26 intermediate typedef for the type of the bound (local to lfp)
2014-02-26 wenzelm 2014-02-26 merged
2014-02-26 wenzelm 2014-02-26 tuned specifications and proofs;
2014-02-26 wenzelm 2014-02-26 more precise before_caret_range (looking both in space and time);
2014-02-26 wenzelm 2014-02-26 improved rendering of blinking cursor;
2014-02-26 wenzelm 2014-02-26 markup for method combinators;
2014-02-26 wenzelm 2014-02-26 tuned;
2014-02-26 wenzelm 2014-02-26 tuned signature;
2014-02-26 wenzelm 2014-02-26 suppress completion of obscure keyword, avoid confusion with plain "simp";
2014-02-26 wenzelm 2014-02-26 method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-26 kuncar 2014-02-26 transfer domain rule for special case of functions - was missing
2014-02-26 boehmes 2014-02-26 replaced smt-based proof with metis proof that requires no external tool
2014-02-26 haftmann 2014-02-26 obsolete workaround
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-26 traytel 2014-02-26 made tactics more robust
2014-02-25 wenzelm 2014-02-25 merged
2014-02-25 wenzelm 2014-02-25 tuned specifications and proofs;
2014-02-25 wenzelm 2014-02-25 merged
2014-02-25 wenzelm 2014-02-25 uniform insert vs. popup policy;
2014-02-25 wenzelm 2014-02-25 tuned proofs;