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;

tuned;

proper support for RAW_ML_SYSTEM;

tuned signature;

separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";