avoid repeated File.read for theory text (as before); misc tuning and simplification;

tuned messages and comments;

simplified Thy_Header.read -- include Source.of_string_limited here; tuned;

simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;

more precise stats;

merged

quickcheck images of goals under registration morphisms

get_registrations interface

restored unusual snd-biased merge/join policy -- required due to non-conservative code setups

merged

reactivated Scala check

corrected range check once more

added Code_Natural.thy

reactivated Scala check; tuned import order

reactivated Scala check

modified namespace policy

use Natural as index type for Haskell and Scala

merged

keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.

first step in using "fof" rather than "cnf" in TPTP problems

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;