tuned whitespace;

HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;

prove Liminf_inverse_ereal

merged

exchange uniform limit and integral

congruence rules for the relator

conceal only the definitional theorems of map, set, rel (and not the actual constants)

more useful properties of the relators

tuned proofs (less warnings)

Useful facts about min/max, etc.

Merge

fixed a VERY SLOW proof

SOME rather than THE makes it easy to prove equivalence with other forms of derivatives

New lemmas

Prepared two non-terminating proofs; no obvious link with my changes

added AVL and lookup function

tuned

merged

unified isin-proofs

tuned

include some data structures into code generation

effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level

tuned references

added red black trees

clarified markup; tuned signature;

isabelle update_cartouches;

merged

tuned GUI;

removed auto update -- bad reactivity;

clarified isabelle.update-state;

more reactive update, like Output panel;

added isabelle update_then;