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;

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

more generous memory settings for scala check

no polymorphic "var"s

merged

adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples

do a better job at Skolemizing in Nitpick, for TPTP FOF

revert code that was submitted by mistake

renamings + only need second component of name pool to reconstruct proofs

rename "classrel" to "class_rel"

rename "combtyp" constructors

renamed "Literal" to "FOLLiteral"

renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators

merged