more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;

HOL-SPARK .prv files are subject to system option spark_prv;
tuned;

dropped obsolete external entrance point

removed non-existing MaSh component from list

tuned comments;

retired wwwfind

--HG--
extra : rebase_source : e6cca658f9383587b1f89e62d8f03c03ed6e0d53

simplified settings for src/HOL/Tools/SMT;

--HG--
rename : src/HOL/Tools/SMT/etc/settings => src/HOL/Tools/etc/settings

system options for Isabelle/HOL proof tools;

removed unused Predicate_Compile component setup;

moved MaSh's Python code into Isabelle

minimal component and build setup for graphview;

fewer components, more roots;

tuned;

always retain doc-src (as regular component);

moved "nitrox" to TPTP

--HG--
rename : src/HOL/Tools/Nitpick/etc/settings => src/HOL/TPTP/etc/settings
rename : src/HOL/Tools/Nitpick/lib/Tools/nitrox => src/HOL/TPTP/lib/Tools/nitrox

build jedit as part of regular startup script (in that case depending on jedit_build component);
misc tuning and simplification;

--HG--
rename : src/Tools/jEdit/dist-template/etc/isabelle-jedit.css => src/Tools/jEdit/etc/isabelle-jedit.css
rename : src/Tools/jEdit/dist-template/etc/settings => src/Tools/jEdit/etc/settings
rename : src/Tools/jEdit/dist-template/lib/Tools/jedit => src/Tools/jEdit/lib/Tools/jedit

added "nitrox" tool (Nitpick for first-order TPTP problems) to components

renamed Sum_Of_Squares to Sum_of_Squares;

--HG--
rename : src/HOL/Library/Sum_Of_Squares.thy => src/HOL/Library/Sum_of_Squares.thy
rename : src/HOL/Library/Sum_Of_Squares/etc/settings => src/HOL/Library/Sum_of_Squares/etc/settings
rename : src/HOL/Library/Sum_Of_Squares/neos_csdp_client => src/HOL/Library/Sum_of_Squares/neos_csdp_client
rename : src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML => src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
rename : src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML => src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
rename : src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML => src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

adding mutabelle as a component and an isabelle tool to be used in regression testing

removed HOLCF for now as explicit component

registering code_prolog as component; using environment variable; adding settings file for prolog code generation

updated component name

integrated SMT into the HOL image

removed Cache_IO component

added Cache_IO: cache for output of external tools,
changed SMT solver interface to use Cache_IO

WWW_Find component: find_theorems via web browser

--HG--
extra : rebase_source : 305553093830012aa175f007d7d552ee4f0a80ca

added new method "smt": an oracle-based connection to external SMT solvers

moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle

--HG--
rename : src/HOL/Tools/Mirabelle/Mirabelle.thy => src/HOL/Mirabelle/Mirabelle.thy
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle.ML => src/HOL/Mirabelle/Tools/mirabelle.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML => src/HOL/Mirabelle/Tools/mirabelle_arith.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML => src/HOL/Mirabelle/Tools/mirabelle_metis.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML => src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML => src/HOL/Mirabelle/Tools/mirabelle_refute.ML
rename : src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML => src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
rename : src/HOL/Tools/Mirabelle/doc/options.txt => src/HOL/Mirabelle/doc/options.txt
rename : src/HOL/Tools/Mirabelle/etc/settings => src/HOL/Mirabelle/etc/settings
rename : src/HOL/Tools/Mirabelle/lib/Tools/mirabelle => src/HOL/Mirabelle/lib/Tools/mirabelle
rename : src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl => src/HOL/Mirabelle/lib/scripts/mirabelle.pl

code generator is now a separate component

--HG--
rename : lib/Tools/codegen => src/Tools/Code/lib/Tools/codegen

tuned;

moved Mirabelle to HOL/Tools

made Mirabelle a component

misc changes to SOS by Philipp Meyer:
CSDP_EXE as central setting;
separate component src/HOL/Library/Sum_Of_Squares;
misc tuning and rearrangement of neos_csdp_client;
more robust treatment of shell paths;
debugging depends on local flag;
removed unused parts;

--HG--
rename : lib/scripts/neos/NeosCSDPClient.py => src/HOL/Library/Sum_Of_Squares/neos_csdp_client
rename : src/HOL/Library/sos_wrapper.ML => src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
rename : src/HOL/Library/sum_of_squares.ML => src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML

src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;

--HG--
rename : lib/scripts/SystemOnTPTP => src/HOL/Tools/ATP_Manager/SystemOnTPTP
rename : src/HOL/Tools/atp_manager.ML => src/HOL/Tools/ATP_Manager/atp_manager.ML
rename : src/HOL/Tools/atp_minimal.ML => src/HOL/Tools/ATP_Manager/atp_minimal.ML
rename : src/HOL/Tools/atp_wrapper.ML => src/HOL/Tools/ATP_Manager/atp_wrapper.ML

turned object-logics into components;
isabelle makeall: operate on all components with IsaMakefile, not just hardwired "logics";