added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; recovered printing of Hoare assign statements from 45d090186bbe;

tuned;

dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

more direct loose_bvar1; tuned;

indentation;

update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);

added editor mode line;

isolate change of Proofterm.proofs in TPTP.thy from rest of session; qualified Proofterm.proofs to facilitate grepping;

list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin; exclude backup files;

updated contributed components

Z3 non-commercial usage may explicitly be declined

export status function to query whether Z3 has been activated for usage within Isabelle

merge

avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"

move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle

really be quiet

replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH

merged

standardized headers

generalized Caratheodory from algebra to ring_of_sets

add ring_of_sets and subset_class as basis for algebra

added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter

added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers

remove lie from documentation

let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now

make Minimizer honor "verbose" and "debug" options better

fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples

moved some configurations to AFP, and fixed others

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;

binder_tr: more informative exception;

Hoare syntax: strip positions where they crash translation functions; re-unified some clones (!);

update_name_tr: more precise handling of explicit constraints, including positions;

statespace syntax: strip positions -- type constraints are unexpected here;

let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);

datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";

tuned indendation and parentheses;

support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;

pretty_string: proper handling of negative max_len;

added Lexicon.encode_position, Lexicon.decode_position;

tuned;

tuned;

clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;

tuned;

merged

added judgement day configurations

another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);

fixed perl error

eliminated unnecessary generated ROOT.ML

more precise dependencies

small test case for main mirabelle functionality, which easily breaks without noticing

propagate mirabelle failures properly; flatten obscure return code semantics of Perl system command to 0/1

mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)

merged

adapting predicate_compile_quickcheck; tuned

adapting mutabelle

adapting SML_Quickcheck

passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing

extending the test data generators to take the evaluation terms as arguments

adding option of evaluating terms after invocation in quickcheck

adding eval option to quickcheck

handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation

adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing

adding a simple datatype for representing functions in Quickcheck_Narrowing

extending code_int type more; adding narrowing instance for type int; added test case for int instance

translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases

adding size as static argument in quickcheck_narrowing compilation

modernized specifications;

dropped unused structure aliases;

tuned;

NEWS: structure Timing provides various operations for timing;

simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);

pure Timing.timing, without any exception handling; clarified cond_timeit: propagate interrupt without side-effect;

structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;

pervasive cond_timeit;

eliminated dead code;

parallel preparation of document variants, within separate directories;

Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections; tuned;

eliminated redundant doc_prefix1; tuned;

renamed doc_prefix2 to dump_prefix;

tuned;

tuned terminology for document variants;

replaced File.check by specific File.check_file, File.check_dir; clarified File.full_path -- include parts of former Thy_Load.get_file; simplified Thy_Load.check_file -- do not read/digest yet; merged Thy_Load.check_thy/deps_thy -- always read text and parse header; clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator; Thy_Info.check_deps etc.: File.read exactly once;

tuned;

preencode value of "need" selectors in Kodkod bounds as an optimization

ignore "need" axioms for "nat"-like types

added "simp:", "intro:", and "elim:" to "try" command

optimize Kodkod axioms further w.r.t. "need" option

optimize Kodkod bounds of nat-like datatypes

more optimizations of bounds for "need"

optimize Kodkod bounds when "need" is specified

always destroy constructor patterns, since this seems to be always useful

reintroduced "show_skolems" option -- useful when too many Skolems are displayed

reword Nitpick's wording concerning potential counterexamples

prevent an exception if "card" is empty (e.g., "nitpick [card]")

add option to function to keep trivial ATP formulas, needed for some experiments

add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)

tuned lemma

added lemmas

added lemma

support non-ground "need" values

recover Isabelle symlink for public distribution, notably website;

standardized headers;

merged

reworked Probability theory: measures are not type restricted to positive extended reals

split Extended_Reals into parts for Library and Multivariate_Analysis

lemmas about addition, SUP on countable sets and infinite sums for extreal

add infinite sums and power on extreal

introduce setsum on extreal

use abs_extreal

simplified definition of open_extreal

use case_product for extrel[2,3]_cases

add Extended_Reals from AFP/Lower_Semicontinuous

add lemmas for monotone sequences

add lemmas for SUP and INF

generalize infinite sums

moved t2_spaces to HOL image

example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;

isatest: fresh copy of settings avoids odd cumulative environment;

tuned exhaustive_generators

removing definition of cons0; hiding constants in Quickcheck_Narrowing

tuned subsubsection names in Quickcheck_Narrowing

tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)

correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing

renaming series and serial to narrowing in Quickcheck_Narrowing

eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;

tuned headers;

eliminated hard tabs;

less ambitious isatest;

modernized imports (untested!?);

files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;

explicit type SHA1.digest;

slightly more robust bash exec, which fails on empty executable;

cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime;

some cleanup of old-style settings;

clarified ISABELLE_CSDP setting (formerly CSDP_EXE);

more conventional Mutabelle settings -- similar to Mirabelle;

more basic use of Path.position/File.read;

prefer qualified ISABELLE_NEOS_SERVER;

proper File.shell_path;

more conventional variable name;

Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;

fixed document;

isatest: test more external code;

tuned headers;

allow spaces in executable names; simplified generated bash scripts;

tuned;

tuned headers;

adapting example file to renaming of the quickcheck tester

renaming tester from lazy_exhaustive to narrowing

minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common

renaming example file correctly

adapting Main file generation for Quickcheck_Narrowing

adapting Quickcheck_Narrowing and example file to new names

renaming LSC_Examples theory to Quickcheck_Narrowing

renaming lazysmallcheck ML file to Quickcheck_Narrowing

renaming LSC to Quickcheck_Narrowing

adaptions in generators using the common functions

adding file quickcheck_common to carry common functions of all quickcheck generators

adapting record package to renaming of quickcheck's structures

moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better

correcting dependencies in IsaMakefile

renaming signatures and structures; correcting header

adapting Quickcheck theory after moving ML files

moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML

moving exhaustive_generators.ML to Quickcheck directory

correcting dependencies after renaming

replacing naming of small by exhaustive

renaming smallvalue_generators.ML to exhaustive_generators.ML

renaming constants in Quickcheck_Exhaustive theory

renaming Smallcheck to Quickcheck_Exhaustive

only testing theory LSC_Examples when GHC is installed on the machine

increasing timeout of example for counterexample generation

adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC

adding lazysmallcheck example theory to HOL-ex session

adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies

replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype

changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent

adding an example theory for Lazysmallcheck prototype

adding Lazysmallcheck prototype to HOL-Library

adding files for prototype of lazysmallcheck

removing debug message in quickcheck's postprocessor

fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample

renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck

improving term postprocessing for counterexample presentation in quickcheck

tuned

finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)

improved formula for specialization, to prevent needless specializations -- and removed dead code

perform no arity check in debug mode so that we get to see the Kodkod problem

spark_end now joins proofs of VCs before writing *.prv file.

clarified

produce helpful mira summary for more errors

eliminated prems;

eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;

tuned proofs -- eliminated prems;

merged

merged

don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on

simplified Thy_Info.check_file -- discontinued load path;

discontinued legacy load path;

re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;

modernized imports;

observe standard header format;

removed spurious 'unused_thms' (cf. 1a65b780bd56);

isatest cygwin-poly-e: new memory management of polyml-svn could be more stable;

merged

merged

- Made sure that sort_defs is aware of constants introduced by add_type_def - add_def now compares Isabelle types rather than SPARK types to ensure that type abbreviations are taken into account

mention new Nitpick options

simplify "need" option's syntax

renamed "preconstr" option "need"

finally remove upper_bound_finite_set

separate settings for afp test

added missing spaces in output

lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on

unfold definitions in "preconstrs" option

robust handling of types occurring in "eval" and "preconstr" options but not in the goal

make "preconstr" option more robust -- shouldn't throw exceptions

merged

merged

declare ext [intro]: Extensionality now available by default

merged

removed dependency on Dense_Linear_Order

adding function Quickcheck.test_terms to provide checking a batch of terms

adding a function to compile a batch of terms for quickcheck with one code generation invocation

improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)

made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"

if "total_consts" is set, report cex's as quasi-genuine

document new "total_consts" option

added "total_consts" option

added a few lemmas by Andreas Lochbihler

Corrected HOLCF/FOCUS dependency

Added material by David Trachtenherz

corrected HOLCF dependency on Nat_Infinity

got rid of lemma upper_bound_finite_set

merged

Some cleaning up

updated generated files

fixed manual (rule no longer exists)