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

adding mode inference to prolog compilation; separate between (ad-hoc) code modifications and system_configuration; adapting quickcheck

merged

tidied a few proofs

merged

avoid code duplication

tuning

merge constructors

factor out the inverse of "nice_atp_problem"

use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs

factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"

prevent exception when calling "Mirabelle.can_apply" on empty proof sequence; the Judgement Day logs sometimes had entries of the form at 970:26 (apply): ------------------ ------------------ ; these were apparently caused by this Mirabelle bug

supply the Metis parameter defaults as argument, instead of patching the Metis sources; these values were found by Larry in 2007 and using anything else risks losing proofs

regenerated "metis.ML"

streamlined "make_metis"

put Isabelle-specifics in a "PortableIsabelle" file maintained by us; as recommended by Joe Hurd

handy little script

reintroduce missing "critical"s by hand

MIT license -> BSD License

copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle

tuned;

allow embedded reports in regular prover messages, to avoid side-effects for errors for example;

simplified/clarified (Context_)Position.markup/reported_text;

eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;

Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);

updated generated file;

tuned whitespace

reverse order of datatype declarations so that declarations only depend on already declared datatypes

merged

make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; instead, query the original "Makefile"

dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;

merged

document Metis updating procedure

move "CRITICAL" to "PortableXxx", where it belongs and used to be; now that it is no longer used in "Random.sml"

regenerated "metis.ML"

update comment

make "Unprotected concurrency introduces some true randomness." be true; this code is called often and doesn't need to be considered critical. I added CRITICAL by mistake.

fix parsing of higher-order formulas; this code was never exercised before because the current ATPs perform clausification, but someday ATPs might support FOF natively

merged

load code_runtime immediately again

proper interface for code_reflect

introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy

merged

"Metis." -> "Metis_" to reflect change in "metis.ML"

no need for "metis_env.ML" anymore; it was a neat solution but it didn't work anymore once I removed the "structure Metis"

regenerate "metis.ML", this time without manual hacks

remove needless file for us

got rid of three crude regexps from "make_metis"

more Isabelle-specific changes

tuning

rename

use "Metis_" prefix rather than "Metis" structure; the prefix can then be used not only for structures but also signatures and functors. A few other changes were made to the script, to eliminate the need for "metis_env.ML".

no need for TPTP

put "foldl" and "foldr" in "Useful"; Isabelle hides those symbols from List, but by adding them to Useful we have them throughout Metis without "List." prefix

reintroduce the CRITICAL sections from change 3880d21d6013

apply Larry's hacks directly to the "src" files; these hacks modify the defaults of Metis heuristics and are necessary for backward compatibility

"FILES" is not (anymore?) part of the official Metis sources, so move it up

merged

Code_Runtime.value, corresponding to ML_Context.value; tuned

Code_Runtime.value, corresponding to ML_Context.value