precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis

clearer terminology

renamed "heavy" to "uniform", based on discussion with Nick Smallbone

removed unused configuration option

added caching for (in)finiteness checks

remove needless typing information

cleaner handling of polymorphic monotonicity inference

started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone

more precise warning

added option to control soundness of encodings more precisely, for evaluation purposes

make sound mode more sound (and clean up code)

reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false

gracefully handle empty SPASS problems

pass sound option to Sledgehammer tactic

tuned signature -- contrast physical output primitives versus Output.raw_message;

tuned signature;

discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);

some support for toplevel printing wrt. editor perspective (still inactive);

propagate editor perspective through document model;

some support for editor perspective;

discontinued redundant Edit_Command_ID;

reduced warnings;

tuned message;

old-style numbered structure index is legacy feature (hardly ever used now);

added official Text.Range.Ordering; some support for text perspective;

tuned signature;

reverted some odd changes to HOL/Import (cf. 74c08021ab2e);

merged

modernized specifications

removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy

removed technical or trivial unused facts

more precise authors and comments; tuned order and headers

added proof of idempotence, roughly after HOL/Subst/Unify.thy

tuned proofs, sledgehammering overly verbose parts

tuned notation

ported some lemmas from HOL/Subst/*; tuned order

changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.

merged

add lemmas interior_Times and closure_Times

avoid pred/set mixture

avoid pred/set mixture

merged

remove unnecessary euclidean_space class constraints

section -> subsection

scale dependency graph to fit on page

more robust initialization of token marker and line context wrt. session startup;

tuned Parse.group: delayed failure message;

avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;

default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;

tuned;

discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;

discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;

merged

replace lemma realpow_two_diff with new lemma square_diff_square_factored

remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff

move lemma add_eq_0_iff to Groups.thy

remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead

rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy

add lemma power2_eq_iff

remove some over-specific rules from the simpset