more canonical context threading

merged

documentation for "Semantic subtype definitions"; misc tuning and simplification;

moved remaining display.ML to more_thm.ML;

less redundant output;

proper context;

tuned;

tuned;

tuned;

tuned signature: eliminated pointless type Context.pretty;

more explicit Defs.context: use proper name spaces as far as possible;

explicit indication of overloaded typedefs;

tuned signature;

tuned output;

tuned output;

tuned signature;

eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;

tuned signature;

tuned output;

separate command 'print_definitions';

tuned;

clarified deps entry: global names for arguments;

renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing;

tuned signature;

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;

NEWS;

tuned priority (like other query operations, e.g. "find_theorems");

option editor_output_state;

obsolete, superseded by State panel;