raising an exception instead of guessing some reasonable behaviour for this function

using linear find_least instead of sorting in the mode analysis of the predicate compiler

adding code attribute to definition of equality of finite sets for executability of equality of finite sets

adapting example files

adding the Reg_Exp example

towards time limiting the prolog execution

adding IMP quickcheck examples

adding the CFG example to the build process

adding a List example (challenge from Tobias) for counterexample search

adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog

disposed some old TODO/FIXME;

Document_View: select gutter message icons from markup over line range, not full range results; tuned;

tuned properties;

moved token markup tables to isabelle_markup.scala;

concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default; tuned Snapshot.convert/revert;

Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;

basic support for warning/error gutter icons;

Document_View: some markup for main inner syntax categories;

Command.State.accumulate: check actual source range;

Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

highlight bad range of nested error (here from inner parsing);

Isar_Document.reported_positions: exclude proof state output;

Document_View: less aggressive background coloring, departing from classic PG highlighting; tuned colors;

report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase; tuned color;

slightly more robust Plugin.stop -- components might refer to Isabelle.system even after shutdown;

turned show_hyps and show_tags into proper configuration option;

discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;

ML_Context.thm and ML_Context.thms no longer pervasive;

more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;

merged

When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.

isatest: back to polyml-5.3.0 due to unresolved stability issues of polyml-5.4.0 and HOL/Decision_Procs/Approximation_Ex.thy;

more antiquotations;

ML_Context.thm;

more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);

modernized session ROOT setup;

some results of concurrency code inspection;

merged;

mention ~/.isabelle/etc/settings file

make remote ATP invocation work for those people who need to go through a proxy; thanks go to Mathieu G. for that fix

enabled do notation for option type

removed duplicate lemma

added Option.bind

merged

printing combinator for hierarchical programs

merged

add lemma cont2cont_Let_simple

add lemma cont2cont_split_simple

add List_Cpo.thy to HOLCF/Library

dropped names from serializer interface

added more explicit warning

ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;

use setmp_noncritical for PGIP, which is presumably sequential (PG clone);

use setmp_noncritical for sequential Pure bootstrap;

turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;

Syntax.standard_parse_term: eliminated redundant Pretty.pp;

structure Syntax: define "interfaces" before actual implementations;

turned show_sorts/show_types into proper configuration options;

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

refined treatment of multi-line subexpressions;

basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);

updated configuration options;

recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);

turned eta_contract into proper configuration option;

turned show_structs into proper configuration option;

configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;

pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;

tuned comment;

merged

merged

QND_FLAG is a shell variable, not a string

modernized session ROOT;

disposed left-over user preferences;

turned show_all_types into proper configuration option;

treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;

more explicit Config.declare vs. Config.declare_global;

turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;

remove code I submitted accidentally

merged

disable "definitional CNF"; it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method

redisable Nitpick from Cygwin, until I've investigated the issue

show the number of facts for each prover in "verbose" mode

fix bug in "debug" mode

make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread

If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user

fix trivial "x = x" fact detection

merged

merged

merged

hand out deresolver from serializer invocation

Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)

merged

Updated proofs in Dining Cryptographers theory

Corrected definition and hence removed sorry.

Moved lemmas to appropriate locations

merged

merged

measure unique

merge

move lemmas to correct theory files

factorizable measurable functions

Introduced sigma algebra generated by function preimages.

vimage of measurable function is a measure space

Measurable on product space is equiv. to measurable components

Measurable on euclidean space is equiv. to measurable components

preimages of open sets over continuous function are open

added definition of conditional expectation

proved existence of conditional expectation

introduced integration on subalgebras

changed definition of dynkin; replaces proofs by metis calles

dynkin

dynkin system

merged

Fixes lemma names

NEWS

Introduce surj_on and replace surj and bij by abbreviations.

Permutation implies bij function

bij <--> bij_betw

Add filter_remove1