fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs

use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...

beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)

minor doc fixes

adapt to new type system names

restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"

take "partial_types" option with a grain of salt

fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings

close formula universally, to make SPASS happy

fixed embarrassing bug where conjecture and fact offsets were swapped

pick up GaveUp error on SystemOnTPTP

avoid trailing digits for SNARK (type) names -- grr...

document new type system syntax

use ! for mildly unsound and !! for very unsound encodings

use new type system syntax

implement the new ATP type system in Sledgehammer

define type system in ATP module so that ATPs can suggest a type system

made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support

merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off

drop even more bound types in symbol declarations -- useful in particular for type system "Args true"

tuning

got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly

drop "fequal" type args for unmangled type systems

recognize more SystemOnTPTP errors

cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0

make sure that fequal keeps its type arguments for mangled type systems

no needless "fequal" proxies if "explicit_apply" is set + always have readable names

shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs

avoid Type.TYPE_MATCH exception for "True_or_False" for "If"

proper handling of partially applied proxy symbols

make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type

improve helper type instantiation code

killed needless datatype "combtyp" in Metis

have properly type-instantiated helper facts (combinators and If)

don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set

better known failure recognition for ToFoF-E

cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation

fixed min-arity computation when "explicit_apply" is specified

fixed "tags" type encoding after latest round of changes

more higher-order tests for Sledgehammer/ATP

added friendly hint when Isar proof is missing

fix handling of proxies after recent drastic changes to the type encodings

added a hint to Metis errors suggesting metisFT -- it sometimes work

reconstruct TFF type predicates correctly for ToFoF

fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))

handle special constants correctly in Isar proof reconstruction code, especially type predicates

make sure the minimizer monomorphizes when it should

fixed arity of special constants if "explicit_apply" is set

make sure typing fact names are unique (needed e.g. by SNARK)

minor cleanup

reimplemented the hAPP introduction code so that it's done earlier, when the types are still available

declare TFF types so that SNARK can be used with types

perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it

move type declarations to the front, for TFF-compliance

use postfix syntax for mangled types, for consistency with unmangled

generate typing for "hBOOL" in "Many_Typed" mode + tuning

generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)

improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work

unprefix evil "fof_" prefix inserted by ToFoF

added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format

fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged

generate TFF type declarations in typed mode

no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway

added more rudimentary type support to Sledgehammer's ATP encoding

fixed type of ATP quantifier types (sic)

added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS

added support for TFF type declarations

reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter

added room for types in ATP quantifiers

distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree

remove experimental feature ("risky overload")

added (without implementation yet) new type encodings for Sledgehammer/ATP

close ATP formulas universally earlier, so that we can add type predicates

get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables

renamings

tuned;

include static rail files for old manuals, to make standard make job independent of the "rail" executable;

simplified keyword markup (without formal checking);

treat @ as separate keyword; added @'text' for \isakeyword markup;

default rail fonts via isabellestyle;

localized \isabellestyle;

misc cleanup;

misc cleanup -- no need to copy style files;

eliminated copies of isabelle style files;

use @{rail} antiquotation (with some nested markup); eliminated separate rail/latex phase;

updated Variable.focus;

allow nested @{antiq} (nonterminal) and @@{antiq} terminal;

tuned;

more robust error handling (NB: Source.source requires total scanner or recover); tuned;

removed old rail.ML;

railroad diagrams in LaTeX as document antiquotation;

more uniform variations of scan_string;

literal facts `prop` may contain dummy patterns;

eliminated slightly odd Proof_Context.bind_fixes; tuned;

merged

Properly treat proof functions with no arguments.

merged

inlined Function_Lib.replace_frees, which is used only once

more precise positions via binding;

clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

tuned signature -- eliminated odd comment;

more informative markup for fixed variables (via name space entry); uniform markup for undeclared entities; tuned;

discontinued obsolete markup;

more precise position information via Variable.add_fixes_binding;

more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;

some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);

reorganized fixes as specialized (global) name space;

export Name_Space.entry_ord;

direct use of Variable.is_fixed;

tuned;

predefined LaTeX macros for \<bind> and \<then>;

eliminated obsolete Function_Lib.frees_in_term; simplified;

more uniform Variable.add_frees/add_fixed etc.;

structure Cla as defined in FOL;

proper antiquotations;

tuned;

modernized Clasimp setup;

simplified Blast setup;

clarified auxiliary structure Lexicon.Syntax;

simplified/modernized method setup;

simplified/modernized method setup;

mark thm tag "kind" as legacy;

mutabelle reports: parse results out of log file

hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;

more precise error positions;

clarified Consts.read_const;

clarified Type.the_decl;

more reports and error positions;

added Name_Space.check/get convenience;

clarified check_simproc (with report) vs. the_simproc; proper report for @{simproc} (NB: ML environment is built in invisible context); only one data slot for this module;

proper binding/report of defined simprocs; tuned signature;

modernized specifications;

tuned signature;

stats for mac-poly-M2;

simplified Data signature;

misc tuning and simplification;

misc tuning;

do not open ML structures;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;

modernized Quantifier1 simproc setup;

tuned signature;

clarified simpset setup; discontinued unused old-style FOL_css;

iterate the unsound-fact-set removal process to recover even more unsound proofs

automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option

automatically retry with full-types upon unsound proof

detect some unsound proofs before showing them to the user

tuning -- local semicolon consistency

tuning

rewording

fixed interaction between monomorphization and slicing for ATPs

cleanup: get rid of "may_slice" arguments without changing semantics

implemented general slicing for ATPs, especially E 1.2w and above

fixed typo in documentation

more robust scanning of iterated comments, such as "(* (**) (**) *)";

discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;

eliminated Display.string_of_thm_without_context; tuned whitespace;

merged;

merged

worked around Kodkodi limitation with parsing {}, where it cannot easily deduce its arity -- without this workaround, Kodkod sometimes generates arity errors in conjunction with the "need" option since change 614ff13dc5d2

adding two further code-generator internal constants to the blacklist of Mutabelle

adding examples for Quickcheck used within locales

handling the case where quickcheck is used in a locale with no known interpretation user-friendly

added template diff against newer mercurials, where the 'ago' duplication has been fixed

use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations

hg template diff: renamed to reflect the base version (which silently changed in caf19101073d, by accident?)

standardized some ML aliases;

avoid Display.string_of_thm_without_context; tuned readability of sources;

eliminated global references / critical sections via context data; misc tuning and modernization;

explicit context for Codegen.eval_term etc.;

added Theory.nodes_of convenience;

updated reference machines;

migrated macbroy6 to macbroy30, which is the new "mobile" server (2 cores, 4 GB, Mac OS 10.5);

merged

increase "auto"'s timeout in example to help SML/NJ

making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement

merged

avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary

merged

- renamed enum type class to spark_enum, to avoid confusion with enum type class defined in Enum theory - renamed theorem ..._card_UNIV to ..._card

use "Spec_Rules" for finding axioms -- more reliable and cleaner

optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer

remove a few Nitpick calls in examples -- another step toward making them run faster

check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC

eliminated Codegen.mode in favour of explicit argument;

less bulky "_position", for improved readability of parse trees;

added more elementary Skip_Proof.make_thm_cterm;

explicit markup for loose bounds;

prefer internal types, via Simple_Syntax.read_typ;

eliminated obsolete Proof_Syntax.strip_sorts_consttypes;

split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;

minor tuning and modernization;

slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;

updated some theory primitives, which now depend on auxiliary context;

more precise treatment of existing type inference parameters; tuned;

pretty_abbrev: read abbreviation more directly;

tuned signature;

raised timeouts further, for SML/NJ!

Package prefix is now taken into account when looking up user-defined types and proof functions.

merged

recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);

scheduler for Mutabelle regression

tool for importing nightly isatest logs

adding bounded_forall tester

creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned

pass plain Proof.context for pretty printing;

standardized aliases of operations on tsig;

pass plain Proof.context for pretty printing;

tuned;

simplified Sorts.class_error: plain Proof.context; tuned;

pass plain Proof.context for pretty printing;

simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;

provide structure Syntax early (before structure Type), back-patch check/uncheck later;

added Binding.print convenience, which includes quote already;

markup attributes/methods via name space; eliminated obsolete markup;

tuned signature;

markup facts via name space; eliminated obsolete markup;

tuned -- order in memory according to variance;

eliminated obsolete markup -- superseded by generic "entity" markup;

report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;

clarified pretty_parsetree: suppress literal tokens;

PARALLEL_GOALS for simplification within auto_tac;

PARALLEL_GOALS for method "simp_all";

enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);

refined PARALLEL_GOALS;

tuned blast: navigate to subgoal only once;

proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;

more direct Thm.cprem_of (with exception THM instead of Subscript); modernized thy;

more direct Thm.cprem_of (with exception THM instead of Subscript);

more direct Logic.dest_implies (with exception TERM instead of Subscript);

eliminated old List.nth; tuned;

do not open ML structures;

observe firm naming convention ctxt: Proof.context;

modernized structure Proof_Context;

modernized structure Proof_Context;

prefer local name spaces; tuned signatures; tuned;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

tuned signature, disentangled dependencies;

Added command for associating user-defined types with SPARK types.

turn YXML.parse_file into a fold

nicer error message from Metis for know failure that isn't the user's fault

correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"

tuning

remove needless export

more clausification tests

make 48170228f562 work also with "HO_Reas" examples

improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)

properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code

remove experimental code added in 85bb6fbb8e6a

added examples of definitional CNF facts

"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now

compile

handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377

removed obsolete Skolem counter in new Skolemizer

added outstanding issue to Metis example

use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms

started clausifier examples

make new Skolemizer work also for "metisFT"

improve definitional CNF on goal by moving "not" past the quantifiers

experiment with definitional CNF

use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer

try to repair out-of-sync situations in Metis

handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used

Add YXML.parse_file to signature ...

Add YXML.parse_file to parse and process big data files

Generalized File.fold_lines to File.fold_fields

more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;

Name_Space.entry_markup: keep def position as separate properties; uniform treatment of ML_def/ML_open/ML_struct as entities; hyperlinks for all entities -- excluding ML_open/ML_struct for now;

some position reports for 'translations';

made SML/NJ happy;

merged

added SMT certificates

use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)

fixed eta-expansion: use correct order to apply new bound variables

check if negating the goal is possible (avoids CTERM exception for Pure propositions)

unfold and eta-contract let expressions before lambda-lifting to avoid bad terms

corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables

merged

deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments

generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations

correcting constant name in exhaustive_generators

switching fast compilation off by default for now in exhaustive quickcheck

ensuring datatype limitations before the instantiation in quickcheck_exhaustive

rational and real instances for new compilation scheme for exhaustive quickcheck

splitting exhaustive and full_exhaustive into separate type classes

removing duplicate code

revisiting mk_equation functions and refactoring them in exhaustive quickcheck

creating a general mk_equation_terms for the different compilations

adding an even faster compilation scheme

theory definitions for fast exhaustive quickcheck compilation

new compilation for exhaustive quickcheck

tuned;

present type variables; tuned;

unparse: more accurate markup for syntax consts, notably binders;

notation: proper markup for type constructor / constant;

tuned signature;

more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;

discontinued Syntax.max_pri, which is not really a symbolic parameter;

CONST syntax with positions;

moved CONST syntax/translations to their proper place;

simplified Pure syntax bootstrap;

renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;

merged

raised timeout further, for SML/NJ

discontinued special treatment of structure Lexicon;

discontinued special status of structure Printer;

discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;

discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;

more antiquotations;

removed outdated text (cf. 84a3f86441eb);

explicit structure Syntax_Trans; discontinued old-style constrainAbsC;

tuned presentation;

report literal tokens according to parsetree head; some attempts to stack parsetrees in proper order;

simplified read_term vs. read_prop;

tuned signature;

constant =?= no longer exists (cf. 8c09e1fa24a7);

clarified sources -- removed odd comments;

tuned signature;

merged

removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1

removing instantiation exhaustive for unit in Quickcheck_Exhaustive

correcting bounded_forall construction; tuned

dropped unused lemmas; proper Isar proof

further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind

make new Skolemizer more robust

tuned comment

discontinued user-defined token translations; tuned signature;

simplified printer context: uniform externing and static token translations;

clarified Pretty.mark; added Pretty.mark_str, Pretty.marks_str convenience;

parallel parsing of big specifications;

separate structure Term_Position; dismantled remains of structure Type_Ext;

type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);

moved type syntax translations to syn_trans.ML;

made SML/NJ happy (cf. 578a51fae383);

merged

merged

changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)

prove measurable_into_infprod_algebra and measure_infprod

Rename extensional to extensionalD (extensional is also defined in FuncSet)

eliminated slightly odd Syntax.rep_syntax;

more abstract print translation;

more abstract syntax translation;

tuned;

explicit Syntax.tokenize, Syntax.parse;

eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem;

simplified standard parse/unparse;

discontinued old-style Syntax.constrainC;

typed_print_translation: discontinued show_sorts argument;

misc tuning and simplification;

moved unparse material to syntax_phases.ML;

more symbol abbrevs;

renamed Standard_Syntax to Syntax_Phases;

moved decode/parse operations to standard_syntax.ML; tuned;

separate module for standard implementation of inner syntax operations;

moved Isar/local_syntax.ML to Syntax/local_syntax.ML;

merged

added "no_atp" to Cantor's paradox

renamed "const_args" option value to "args"

temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception

updated instructions

minor doc edits

killed unimplemented type encoding "preds"

remove debugging code

removing bounded_forall code equation for characters when loading Code_Char

deriving bounded_forall instances in quickcheck_exhaustive

generalizing ensure_sort_datatype for bounded_forall instances

document "type_sys" option

if "monomorphize" is enabled, mangle the type information in the names by default

use standard tables with standard argument order;

discontinued special treatment of structure Parser -- directly accessible;

discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

more precise propagation of reports/results through some inner syntax layers; misc reorganization;

accumulate parsetrees in canonical reverse order;

tuned;

tuned -- removed redundancy;

tuned signatures;

streamlined token list operations, assuming that the order of union does not matter;

misc tuning and clarification;

merged

document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"

refactoring generator definition in quickcheck and removing clone

use the proper contexts/simpsets/etc. in the TPTP proof method

merged

make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option

merged

Deletion of all semicolons, because they interfere with Proof General

raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.

tuned proofs

tuned proof

direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;

added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;

show more tooltip/sub-expression markup;

show tooltip/sub-expression for entity markup;

merged

remove unnecessary prob_preserving

add prob_space_vimage

use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);

fixed accidental redefinition

save reflexivity steps in discharging Z3 Skolemization hypotheses

adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall

adding general interface for batch validators in quickcheck

remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428

scheduler for judgement day

re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end

make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option

merged

adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy

raised timeouts further, for SML/NJ

adapted parsing of session timing (cf. e86b10c68f0b)

merged

adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily

provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)

start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)

temporary workaround: filter out spurious monomorphic instances

added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default

added support for "dest:" to "try"

corrected infix precedence for boolean operators in Haskell

merged

removing dead code in exhaustive_generators

removing junk that should not have been committed

modernized specifications;

accomodate autofix discipline of non-body context;

session timing: show pseudo-speedup factor;

visualize skolem and hilite (undeclared frees); tuned colors;

more informative markup_free;

inline lemmas instead of accidental physical addressing -- explicit is better than implicit;

tuned white space and indentation; observe strict line length limitation (80-100 chars);

actually check list comprehension examples;

products of probability measures are probability measures

real multiplication is continuous

add lebesgue_real_affine

renewing specifications in HOL: replacing types by type_synonym

moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure

adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape

NEWS

generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities

merged

added missing smlnj target

modernized specifications -- less axioms;

modernized specifications -- some attempts to avoid wild axiomatizations; comp: retain infix \<circ> to retain type "o" from FOL; tuned proofs;

tuned proofs;

use shared copy of hoare_syntax.ML; misc tuning;

Hoare syntax: standard abstraction syntax admits source positions; re-unified some clones (!);

tuned headers;

tuned headers;

NEWS

rename Probability_Space to Probability_Measure

add infinite product measure

split Product_Measure into Binary_Product_Measure and Finite_Product_Measure

proved caratheodory_empty_continuous

list comprehension: strip positions where the translation cannot handle them right now;

address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;

raised various timeouts to accommodate sluggish SML/NJ

changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ

keep smlnj HOL images around

merged

added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall

avoid *** in normal output, which usually marks errors in logs

added Markup.Name and Markup.Kind convenience; token_style for entity kind markup;

decode_term: some context-sensitive markup; more informative Markup.entity and Name_Space.markup_entry; Markup.const: use "constant" to make it coincide with name space kind;

tuned signatures;

decode_term: more precise reports;

adhoc token style for free/bound;

decode_term/disambig: report resolved term variables for the unique (!) result;

removed unclear comments stemming from ed24ba6f69aa;

present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;

added Future.cond_forks convenience;

Isabelle_System.create_tmp_path/with_tmp_file: optional extension; thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;

tuned;

more direct loose_bvar1; tuned; slight re-unification of clone (cf. 47f8bfe0f597);

suppress Mercurial backup files; uniform treatment of tool filtering in bash/perl/scala;

updated generated file; tuned whitespace;

merged

SML_makeall: run with -j 3

fixed incomplete rename (1cdf54e845fa)

eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)

merged

changing iteration scheme of functions to use minimal number of function updates for exhaustive testing

added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)

mira interface to 'isabelle make' in addition to usedir and makeall; do not require dependencies