2010-08-17 haftmann 2010-08-17 formally document `code abstype` and `code abstract` attributes
2010-08-17 haftmann 2010-08-17 NEWS and CONTRIBUTORS
2010-08-17 haftmann 2010-08-17 nicer code for rev
2010-08-17 haftmann 2010-08-17 reworked section on simple datatype refinement
2010-08-17 haftmann 2010-08-17 tuned whitespace
2010-08-17 blanchet 2010-08-17 merged
2010-08-16 blanchet 2010-08-16 typos in comment
2010-08-16 blanchet 2010-08-16 more debug output
2010-08-16 blanchet 2010-08-16 detect old Vampire and give a nicer error message
2010-08-17 nipkow 2010-08-17 merged
2010-08-17 nipkow 2010-08-17 now works for schematic terms as well, thanks to Alex for the `how-to'
2010-08-17 haftmann 2010-08-17 added section on program refinement
2010-08-17 haftmann 2010-08-17 tuned whitespace
2010-08-17 wenzelm 2010-08-17 tune;
2010-08-17 wenzelm 2010-08-17 added functor Linear_Set, based on former adhoc structures in document.ML; Linear_Set.delete_after (ML): actually delete table entries; Scala Linear_Set: clarified exceptions, according to ML version; simplified Document.node using Linear_Set; ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;
2010-08-16 wenzelm 2010-08-16 HOL-Proofs-Extraction: some workaround to make it work in low-memory situations (e.g. atbroy102 with as little as 1GB heap space);
2010-08-16 wenzelm 2010-08-16 XML.Cache: pipe-lined (thread-safe) version using actor; tuned Isabelle_Process.pid handling;
2010-08-16 wenzelm 2010-08-16 simplified internal message format: dropped special Symbol.STX header;
2010-08-16 wenzelm 2010-08-16 HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
2010-08-16 wenzelm 2010-08-16 merged
2010-08-16 haftmann 2010-08-16 merged
2010-08-16 haftmann 2010-08-16 tuned section on predicate compiler
2010-08-16 haftmann 2010-08-16 section "if something goes utterly wrong"
2010-08-16 haftmann 2010-08-16 merged
2010-08-16 haftmann 2010-08-16 merged
2010-08-16 haftmann 2010-08-16 adaptation to new outline
2010-08-13 haftmann 2010-08-13 merged
2010-08-13 haftmann 2010-08-13 corrected handling of `constrains` elements
2010-08-16 kleing 2010-08-16 removed non-BSD compatible option from cp
2010-08-16 blanchet 2010-08-16 Geoff's formatter now needs closed formulas
2010-08-15 nipkow 2010-08-15 Using type real does not require a separate logic now.
2010-08-15 nipkow 2010-08-15 merged
2010-08-15 nipkow 2010-08-15 tuned text about "value" and added note on comments.
2010-08-16 wenzelm 2010-08-16 simplified command status: interpret stacked markup on demand;
2010-08-15 wenzelm 2010-08-15 event_bus.scala rather belongs to system plumbing;
2010-08-15 wenzelm 2010-08-15 some derived operations on Text.Range;
2010-08-15 wenzelm 2010-08-15 specific types Text.Offset and Text.Range; minor tuning;
2010-08-15 wenzelm 2010-08-15 moved Text_Edit to Text.Edit; tuned;
2010-08-15 wenzelm 2010-08-15 moved History/Snapshot to document.scala;
2010-08-15 wenzelm 2010-08-15 renamed raw_results to raw_protocol;
2010-08-15 wenzelm 2010-08-15 rename "unit" to "atom", to avoid confusion with the unit type;
2010-08-15 wenzelm 2010-08-15 document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
2010-08-15 wenzelm 2010-08-15 use Synchronized.var and prevent global CRITICAL sections in this hot spot;
2010-08-15 wenzelm 2010-08-15 renamed create_id to new_id;
2010-08-15 wenzelm 2010-08-15 more explicit / functional ML version of document model; tuned;
2010-08-15 wenzelm 2010-08-15 renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;
2010-08-15 wenzelm 2010-08-15 fixed Isabelle/Scala build (cf. f3220ef79d51);
2010-08-14 wenzelm 2010-08-14 Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14 wenzelm 2010-08-14 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
2010-08-14 wenzelm 2010-08-14 Keyword.status: always suppress position;
2010-08-14 wenzelm 2010-08-14 moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
2010-08-14 wenzelm 2010-08-14 merged
2010-08-13 haftmann 2010-08-13 robustified proof
2010-08-13 haftmann 2010-08-13 lemma execute_bind_case
2010-08-13 haftmann 2010-08-13 unit and bool are instances of heap
2010-08-13 haftmann 2010-08-13 merged
2010-08-13 haftmann 2010-08-13 sketch of new outline
2010-08-13 haftmann 2010-08-13 sketch of new outline
2010-08-13 haftmann 2010-08-13 ditem
2010-08-13 haftmann 2010-08-13 refined abstract