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

merged

redefine constant 'trivial_limit' as an abbreviation

purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;

refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;

odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);