fix polymorphic "val"

temporarily deactivating check for Scala

another refinement chapter in the neverending numeral story

inductive_cases: crude parallelization via Par_List.map;

modernized/unified some specifications;

Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;

simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; eliminated obsolete touch_child_thys, register_theory;

simplified handling of theory begin/end wrt. toplevel and theory loader;

Thy_Load.check_loaded via Theory.at_end;

tuned;

moved basic thy file name operations from Thy_Load to Thy_Header;

moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;

merged

avoid unreliable Haskell Int type

proper subclass instead of sublocale

repaired tool invocation

observe standard conventions for doc-strings;

tuned message;

eliminated some unused Thy_Info operations;

refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;

generic external source files -- nothing special about ML here;

discontinued special treatment of ML files -- no longer complete extensions on demand; simplified Thy_Load.check_file, with uniform error reporting; added Thy_Load.test_file for non-strict checking; misc tuning and simplification;

eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL; reset_path is CRITICAL;

tuned signature;

updated some headers;

merged

dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)

merged