avoided map_of in def of fun_rep (but still needed for efficient code)

spelling

spelling

tuned

complete revision: finally got rid of annoying L-predicate

moved leastness lemma

proper prolog command-line instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2); speculative update for yap (untested);

use automatic type coerctions in Sqrt example

make SML/NJ happy;

not all Nitpick 'constructors' are injective -- careful

added another definition snipped

actually fail on prolog errors -- such as swipl startup failure due to missing shared libraries -- assuming it normally produces clean return code 0;

modifiers for classical wrappers operate on Proof.context instead of claset;

removed historic comments;

tuned exceptions -- avoid composing error messages in low-level situations;

tuned signature; tuned comments;

proper identifiers -- avoid crash of case translations;

reduced duplication

do not add case translation syntax in rep_datatype compatibility mode

run type inference on input to wrap_data

installed case translations in BNF package

tuned

more antiquotations;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;

updated keywords;

merged

merged

obsolete -- tools should refer to proper Proof.context;

discontinued obsolete ML antiquotation @{claset};

added ML antiquotation @{theory_context};

more standard module name Axclass (according to file name);

made SML/NJ happy

generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector

NEWS and CONTRIBUTORS

declaration attribute for case combinators

Handle dummy patterns in parse translation rather than check phase

disallow coercions to interfere with case translations

allow redundant cases in the list comprehension translation

recur in the expression to be matched (do not rely on repetitive execution of a check phase); separate ML-interface function that is not recurring (strip_case)

tuned whitespace

Use Type.raw_match instead of Sign.typ_match

special constant to prevent eta-contraction of the check-phase syntax of case translations

separate data used for case translation from the datatype package

case translations performed in a separate check phase (with adjustments by traytel)

formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;

prefer local context;

proper proof context; removed historic comments;

tuned;

merged

add command timings (like document command status);

tuned signature;

public Isabelle_Process.xml_cache (thread-safe); cache derived status messages;

tuned signature;

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

clarified protocol_message undefinedness;

quote by Alan Kay;

more accurate documentation;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;

more accurate documentation of "(structure)" mixfix;

more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;

tuned comment;

just one syntax category "mixfix" -- check structure annotation semantically;

tuned message;

handle case clashes on Mac file system by encoding goal numbers

avoid duplicate "tcon_" names

smoothly handle cyclic graphs

compile + fixed naming convention

reverted accidental changes to theory file + updated wrt ML file

no need to filter tautologies anymore -- they are prefiltered by "all_facts"'

work on CASC LTB ISA exporter

tuning

add continuous_on rules for products

fixed spelling

move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

improved printing of exception CTERM (see also d0f0f37ec346);

prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);

more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;

discontinued odd magic number, which was once used for performance measurements;

document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);

merged

more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;

try to preserve original linearization

use somewhat lighter encoding

robustness w.r.t. unknown arguments

cleaned

cleaned

tuned

tuned signature -- agree with markup terminology;

unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;

tuned document

tuned

sup on multisets

convenient induction rule

tuned README -- less buzzwords;

more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT);

added missing file;

tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;

tuned signature -- concentrate GUI tools;

tuned signature -- concentrate GUI tools;

separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications; tuned signature;

separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;

tuned imports;

added var_position in analogy to longid_position, for typing reports on input; avoid duplicate token var report;

removed unnerving (esp in jedit) and pointless warning

tuned

merged

tuned;

recover implicit thread position for status messages (cf. eca8acb42e4a);

additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;

more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);

updated comment to 46b90bbc370d;

recovered proper transaction position for Goal.fork error reporting (lost in 8e9746e584c9);

tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);

tuned output -- less bullets;

default implementation of multisets by list with reasonable coverage of operations on multisets

optionalized very specific code setup for multisets

generalized lemma fold_image thanks to Peter Lammich

tuned;

NEWS for 635562bc14ef;