export ML function

added timers to N2M

document that n2m does not depend on most things in fp_sugar in its type

clarified rule structure;

accomodate Isabelle identifiers with subscripts;

more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;

eliminated unused argument (see also 58110c1e02bc);

add le_log_of_power and le_log2_of_power by Tobias Nipkow

unified CHAR with CHR syntax

isabelle process -T THEORY;

proper option -l;

avoid redundant addLeftOfScrollBar;

no dependency on HighlightPlugin, despite e7b2cfcef94c;

observe ML print depth;

clarified print depth;

recovered from Unicode accident in 7248d106c607;

merged

tuned -- fewer warnings;

discontinued slightly odd "secure" mode;

clarified Pretty.T toplevel pp;

clarified modules;

clarified modules;

tuned header;

clarified modules; tuned signature;

@{make_string} is available during Pure bootstrap;

clarified modules;

unused;

hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;

obsolete;

tuned signature;

obsolete;

tuned whitespace;

proper ML type;

merged

move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library

superfluous premise (noticed by Julian Nagele)

added tree lemmas

normalize schematic names since they are used to instantiate the theorem later

more stuff for extended nonnegative real numbers

less preconditions

merged

eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;

pro-forma selection for improved error message;

eliminated without magic name;

NEWS;

always build with full results; always print unfinished sessions;

clarified name;

isabelle process -d; proper args;

tuned signature;

support for Poly/ML heap hierarchy, which saves a lot of disk space;

clarified signature;

tuned signature;

less physical "logic" argument, with option -l like "isabelle console" etc.;

find heaps uniformly via Sessions.Store; tuned;

clarified modules;

clarified modules;

ML save_state under control of Isabelle/Scala;

clarified prompt: "ML" usually means Isabelle/ML;

record stamps of cumulative input heaps; tuned;

Merge

Contractible sets. Also removal of obsolete theorems and refactoring

add measurability rules for ennreal

generalized some Borel measurable statements to support ennreal

rationalisation of theorem names esp about "real Archimedian" etc.

add fixpoint induction principle

generalized ML function

New results about paths, segments, etc. The notion of simply_connected.

Merge

Refactoring (moving theorems into better locations), plus a bit of new material

strengthened tactics

tuned;

tuned signature;

prefer Scala over bash function;

tuned;

clarified env;

unused;

more uniform signature for various process invocations; env refers to full environment, not the update;

tuned;

more theorems on orderings

dropped junk

tuned;

merged

tuned;

clarified cleanup;

more thorough cleanup -- in Scala;

create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);

obsolete (cf. 63a5782c764e);

clarified session build options: already provided by ML_Process; tuned signature;

spelling

model characters directly as range 0..255 * * * operate on syntax terms rather than asts

tuned messages;

tuned message;

generate theorems like 'bool.split_sel'

merged

tuned;

tuned;

upgrade "isabelle build" to Isabelle/Scala;

prefer plain "isabelle" from PATH within Isabelle settings environment;

isabelle_process is superseded by "isabelle process" tool; tuned tool usage; misc updates and tuning of "system" manual;

clarified messages, notably on Windows where CPU time of poly.exe is not measured;

clarified modules;

clarified files;

clarified files;

don't throw an exception when trying to print an error message

eta-expansion done right in "primcorec"

clarified: constructors in the sense of the code generator are not invertible; correct treatment of constructors with same name but different type; moved doubtful comment to corresponding function call

moved

merged

obsolete;

clarified interactive mode, which is relevant for ML prompts;

more careful print_depth on startup;

ignore SIGINT in waiting wrapper process; proper "bash_process.c" and "build" within component;

more robust cleanup; more defensive timing value;

isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");

tuned;

print timing like lib/scripts/timestop.bash;

prefer explicit locale;

bash process with builtin timing;

elapsed time in milliseconds (cf. Time.now in Poly/ML);

support for timing of the managed process;