removed debugging facilities accidentally left in the committed code

more precise dependencies

merged

generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)

moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)

removed old (unused) SMT monomorphizer

added UNION

merged

rename Fin to enat

add ereal to typeclass infinity

add nat => enat coercion

Introduce infinity type class

Rename extreal => ereal

rename Nat_Infinity (inat) to Extended_Nat (enat)

HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.

build an image for HOL-IMP

deactivating quickcheck invocation in this example until the Interrupt issue is understood

removing inner time limits in quickcheck

updating documentation about quickcheck; adding information about try

adapting example in Predicate_Compile_Examples

exporting function in quickcheck; adapting mutabelle script

more information for the user how to deactivate quickcheck_narrowing if he does not want to use it

making messages more informative

only use exhaustive testing in this quickcheck example

parse equalities correctly in Nitrox parser

pass type arguments to lambda-lifted Frees, to account for polymorphism

generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart

avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"

remove offset from Mirabelle output

the HOL4PROOFS setting is actually HOL4_PROOFS

merged

proof tuning

generalization; various notation and proof tuning

avoid misunderstandable names

moved lemmas to appropriate theory

forgotten qualifier

values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations

killed use of PolyML.makestring

added experimental mira configuration for HOL Light importer

allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)

unactivating narrowing-based quickcheck by default

making active configuration public in narrowing-based quickcheck

declare tester in this quickcheck example

adding code equations for partial_term_of for rational numbers

adapting an experimental setup to changes in quickcheck's infrastructure

adding narrowing instances for real and rational

adapting quickcheck based on the analysis of the predicate compiler

adapting prolog-based tester

quickcheck does not deactivate testers if none are given

adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle

renaming quickcheck_tester to quickcheck_batch_tester; tuned

changing parser in quickcheck to activate and deactivate the testers

adapting SML_Quickcheck to new quickcheck infrastructure

enabling parallel execution of testers but removing more informative quickcheck output

changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck

removing generator registration

parametrized test_term functions in quickcheck

adding random, exhaustive and SML quickcheck as testers

more on complement

more on complement

more consistent theorem names

more lemmas about SUP

structuring duals together

merged

more lemmas about Sup

generalized INT_anti_mono

moving UNIV = ... equations to their proper theories

further generalization from sets to complete lattices

fixed lambda-liftg: must ensure the formulas are in close form

ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)

pass kind to lambda-translation function

more refactoring of preprocessing

more refactoring of preprocessing, so as to be able to centralize it

renamed internal data structure

simplify code -- there are no lambdas in helpers anyway

added lambda-lifting to Sledgehammer (rough)

move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons

merged

generalized some lemmas

consolidated bot and top classes, tuned notation

tuned notation

clarified bash_output_fifo;

moved bash operations to Isabelle_System (cf. Scala version);

access to process output stream via auxiliary fifo;

some file and directory operations;

more general bash_process, which allows to terminate background processes as well;

updated to Poly/ML SVN 1328, which is considered 5.4.2;

added File.fold_pages for streaming of large files; prefer \f notation;

tuned;

HOL/Import: Fix errors with _mk_list

Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);

simplified malformed YXML markup -- special controls are visible in IsabelleText font;

less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp;

more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips);

more visible printing of empty binding;

do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;

more quotes;

merged

added missing dependencies; simplified (by overapproximating a bit); alphabetical order

merged

merged

tuned notation and proofs

move error logic closer to user

allow lambda-lifting without triggers

move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)

added option to control which lambda translation to use (for experiments)

fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem

use monomorphic encoding as fallback, since they tend to produce fewer type errors

don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes

clearer unsound message

clarify fine soundness point

always unfold "Let"s is Sledgehammer, Metis, and MESON

unbreak Nitrox's parsing

merged

tuned lemma positions and proofs

tuned notation

uniqueness lemmas for bot and top

adjusted to tightened specification of classes bot and top

moved lemmas bot_less and less_top to classes bot and top respectively

tightened specification of classes bot and top: uniqueness of top and bot elements