Goal.forked: clarified handling of interrupts;

future_job: explicit indication of interrupts;

more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;

synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;

tuned source structure;

bash_output_fifo blocks on Cygwin 1.7.x;

rename_bvs now avoids introducing name clashes between schematic variables

merged

tuned proofs

merged

tuned header

more uniform naming scheme for Inf/INF and Sup/SUP lemmas

removed "extremely ambigous" warning; has been ignored by everyone for years.

misc tuning and clarification;

tuned whitespace;

support local HOATPs

document local HOATPs

workaround THF parser limitation

LEO-II also supports FOF

misc tuning and simplification;

updated documentation of method "split" according to e6a4bb832b46;

updated references to CADE-23

renamed E wrappers for consistency with CASC conventions

updated Sledgehammer docs

add line number prefix to output file name

added "sound" option to Mirabelle

move lambda-lifting code to ATP encoding, so it can be used by Metis

load lambda-lifting structure earlier, so it can be used in Metis

merged

move legacy candiates to bottom; marked candidates for default simp rules

merged

dropped lemmas (Inf|Sup)_(singleton|binary)

dropped lemmas (Inf|Sup)_(singleton|binary)

rename type 'a net to 'a filter, following standard mathematical terminology

HOLCF: fix warnings about unreferenced identifiers

remove duplicate lemmas

merged

fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)

generalize sequence lemmas

generalize more lemmas about compactness

generalize compactness equivalence lemmas

lemma bolzano_weierstrass_imp_compact

class perfect_space inherits from topological_space; generalized several lemmas

merged

import constant folding theory into IMP

make syntax ambiguity warnings a config option

add lemmas INF_image, SUP_image

declare {INF,SUP}_empty [simp]

rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)

standard theorem naming scheme: complex_eqI, complex_eq_iff

moved division ring stuff from Rings.thy to Fields.thy

Library/Product_ord: wellorder instance for products

modernized file proof_checker.ML;

tuned thm_of_proof: build lookup table within closure;

added Reconstruct.proof_of convenience;

ship message in one piece;

misc tuning -- eliminated old-fashioned rep_thm;

modernized strcture Proof_Checker;

less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;

updated imports;

proper signature;

made SML/NJ happy;

slightly more uniform messages;

avoid pointless completion of illegal control commands;

removed old expand_fun_eq

fixed index entry

removed old recdef and types usage

merged

extended user-level attribute case_names with names for case hypotheses

infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names

workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;

updated version information;

fixed document;

tuned order: pushing INF and SUP to Inf and Sup

tuned order: pushing INF and SUP to Inf and Sup

generalized lemmas to complete lattices

merged

replace old SML code generator by new code generator in MicroJava/J

new state syntax with less conflicts

replace old SML code generator by new code generator in MicroJava/JVM and /BV

merged

more fine-granular instantiation

solving duality problem for complete_distrib_lattice; tuned

merged

Pending FDL types may now be associated with Isabelle types as well.

tuned orthography

avoid yet unknown fact antiquotation

NEWS

more specific instantiation

tuned

class complete_distrib_lattice

NEWS

removing value invocations with the SML code generator

removing the SML evaluator

fixed wrong isubs in IMP/Types

Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names

NEWS: fix typo

updated unchecked forward reference

replaced Nitpick's hardwired basic_ersatz_table by context data

NEWS

moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef

moved recdef package to HOL/Library/Old_Recdef.thy

added dynamic ersatz_table to Nitpick's data slot

eliminated obsolete recdef/wfrec related declarations

more consistent naming in IMP/Comp_Rev

merged

tuned proofs

tuned proofs

new theory HOL/Library/Product_Lattice.thy

domain package: more informative error message for illegal indirect recursion

compiler proof cleanup

added helpers for "All" and "Ex"

put parentheses around non-trivial metis call

no needless mangling

resolved code_pred FIXME in IMP; clearer notation for exec_n

clean up temporary directory hack

tuning

fixed lambda concealing

make SML/NJ happy

simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)

document coercions

rudimentary documentation of the quotient package in the isar reference manual

to_nat is injective on arbitrary domains

finite vimage on arbitrary domains

updated Sledgehammer documentation

renamed "preds" encodings to "guards"

more precise dependencies

further worked around LEO-II parser limitation, with eta-expansion

use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)

no need for existential witnesses for sorts in TFF and THF formats

mangle "undefined"

tuning -- remove useless function (at this point combinators are already in)

remove spurious message

give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts

merged

fixed code generator setup in List_Cset

enat is a complete_linorder instance

merged

Add theory for setting up monad syntax for Cset

merged

removing expectations from quickcheck example

adding remarks after static inspection of the invocation of the SML code generator

merged

added operations to Cset with code equations in backing implementations

merged

adjusted to tailored version of ball_simps

adjusted to tailored version of bex_simps

more coherent structure in and across theories

declare "undefined" constant

make compile

thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture

tuning

introduced hybrid lambda translation

avoid needless type args for lifted-lambdas

replacing conversion function of old code generator by the current code generator in the reflection tactic

fixed typo

removing SML_Quickcheck

NEWS

added legacy warning to old code generation evaluation

added legacy warning to old code generation commands

merged

correcting last example in Predicate_Compile_Examples

make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);

more detailed tracing; tuned;

defensive Term_Sharing, to avoid extending trusted code base of inference kernel;

more precise parse_name according to XML standard; tuned performance;

explicit structure ML_System; tunned ML bootstrap;

defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);

tuned;

merged

dropped errorneous hint

moved some lemmas

merged

ereal is a complete_linorder instance

class complete_linorder

make "concealed" lambda translation sound

deactivating all quickcheck invocations until parallel invocation works safely

adapting two examples in Predicate_Compile_Examples

use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned

merge

Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal

add code generator setup and tests for ereal

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

honor the TPTP environment variable as the root of include relative paths -- that's a weird convention but without it Nitrox will fail at CASC

better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6

more exhaustive testing in Nitrox

no timeout for Nitrox

avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty

added arithmetic decision procedure to CASC setup

added some arithmetic functions, for THF with arithmetic

pull in arithmetic theories

cleanly separate TPTP related files from other examples

increasing timeout to avoid spurious failures

merged

more generalization towards complete lattices

experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package

merge

Tuned

more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;

added term_sharing.ML;

recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;

sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;

low-level tuning;

Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one; Sorts.certify_class: prefer the persistent name;

XML.pretty with depth limit;

more thorough Variable.check_name: Binding.check for logical entities within the term language;

tuned;

merged

Update HOLLightCompat

Update files generated in HOL/Import/HOLLight

HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems

ML pp for XML.tree;

made SML/NJ happy;

clarified YXML.detect;

retain some terminology of "XML attributes";

more uniform Properties in ML and Scala;

more uniform Term and Term_XML modules;

more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;

tuned signature -- less cryptic ASCII names;

discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;

added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;

added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;

more precise Symbol_Pos.quote_string;

clarified YXML.embed_controls -- this is idempotent and cannot be nested;

allow empty body for raw_message -- important for Invoke_Scala;

Isabelle string syntax allows literal control characters;

glyphs from DejaVu for ASCII control characters 5, 6, 7, 127, which have a special meaning in Isabelle or Poly/ML;

more precise exceptions;

tuned XML modules;

Quotient example: Lists with distinct elements

merged

explicit code equation for equality

tuned error messages;

tuned;

tuned signature -- corresponding to Scala version;

made SML/NJ happy; tuned error;

more uniform padded_markup, which is important for caret visibility despite absence of markup;

merged

merged

tuned proofs

tuned notation

tuned notation

tuned notation

NEWS;

proper InvocationTargetException.getCause for indirect exceptions; capture hard errors to ensure protocol integrity; tuned error messages;

tuned error message;

tuned signature;

JVM method invocation service via Scala layer;

tuned signature;

some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;

tuned XML.Cache parameters;

some support to invoke Scala methods under program control;

merged;

merged

tuned proofs and notation

more succinct proofs

more succinct proofs

adding a very liberal timeout for values after a test case failed due to the restricted timeout

improved NEWS

NEWS

standardized String.concat towards implode (cf. c37a1f29bbc0)

adding quickcheck examples for evaluating floor and ceiling functions

adding code equations to execute floor and ceiling on rational and real numbers

adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)

inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;

lambda terms with XML data representation in Scala; avoid `class` in signature;

XML data representation of lambda terms;

YXML.string_of_body convenience;

made SML/NJ happy;

tuned signature;

more abstract signature; tuned;

simplified XML_Data;

less currying in Scala;

propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;

echo prover input via raw_messages, for improved protocol tracing;

tuned;

tuned signature;

clarified propagation of node name and header;

more precise treatment of prover definedness;

tuned source structure;

some support for blobs (arbitrary text files) within document nodes;

tuned signature;

moved global state to structure Document (again);

moved Outer_Syntax.load_thy to Thy_Load.load_thy; tuned signatures; tuned module dependencies;

less stateful outer_syntax;

discontinued odd Position.column -- left-over from attempts at PGIP implementation; Position.offset discriminates postions precisely, now also available for Position.line/line_file;

discontinued special treatment of hard tabulators;

eliminated hard tabs;

merged

merged

added translation to fix critical pair between abbreviations for surj and ~=

floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling

standardized String.concat towards implode;

more abstract Thy_Load.load_file/use_file for external theory resources; prefer Boogie_Loader.parse_b2i on already loaded text, bypassing former File.fold_lines optimization;

comment;

clarified Thy_Load.digest_file -- read ML files only once;

tuned signature;

simplified make_option/dest_option; added make_variant/dest_variant -- usual representation of datatypes;

explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;

explicit indication of type Symbol.Symbol;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;

merged

make SML/NJ happier

make SML/NJ happy + tuning

moved ATP dependencies to HOL-Plain, where they belong

better setup for experimental "z3_atp"

64bit versions of some mira configurations

removed unused mira configuration

merged

tuning options to avoid spurious isabelle test failures

clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;

prefer Synchronized.var;

tuned errors; more direct Name.uu_ for dummy abstractions;

record package: proper configuration options;

just one copy of split_args; tuned error message;

merged

rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq

improved translation of lambdas in THF

added generation of lambdas in THF

add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)

simplified Symbol.iterator: produce strings, which are mostly preallocated; eliminated Symbol.CharSequence complications;

tuned comment (cf. e9f26e66692d);

Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;

theory name needs to conform to Path syntax;

hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;

prefer space_explode/split_lines as in Isabelle/ML;

Path.split convenience;

get theory from last executation state; tuned error messages;

explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example); reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);

clarified cancel_execution/await_cancellation;

tuned signature; tuned;

tuned;

re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target

Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);

quasi-static Isabelle_System -- reduced tendency towards "functorial style";

explicit class Counter;

merged

the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})

equalities of subsets of atLeastLessThan

adding documentation of the value antiquotation to the code generation manual

make SML/NJ happy

install case certificate for If after code_datatype declaration for bool

tuned typo

pervasive Basic_Library in Scala; tuned;

some support for theory files within Isabelle/Scala session;

imitate exception ERROR of Isabelle/ML;

eliminated null;

more explicit edit_node vs. init_node; some support for master_dir and header;

tuned signature;

Thy_Header.read convenience;

some support for Session.File_Store;

tuned signature;

eliminated redundant session_ready;

tuned;

uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;

misc tuning;

correction: do not assume that case const index covered all cases

remove illegal case combinators after merge

corrected misunderstanding what `old functions` are supposed to be

centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be

merged