updated generated file;

tuned quickcheck's response

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

merged

replace more uses of 'lemmas' with explicit 'lemma'; replace uses of 'simplified' attribute with 'unfolded'; remove unused intermediate lemmas.

Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.

fix spelling

fix spelling

added IMP/Live_True.thy

replace many uses of 'lemmas' with 'lemma'; remove many unused intermediate lemmas.

prove class instances without extra lemmas

finite class instance for word type; remove unused lemmas

remove unused lemmas

generalize some lemmas

merged

tidied Word.thy; put attributes directly on lemmas instead of using 'declare'; replace various 'lemmas' commands with ordinary 'lemma'.

remove redundant lemma word_diff_minus

remove some duplicate lemmas, simplify some proofs

Quotient_Info stores only relation maps

hiding definitional facts in Quickcheck; introducing catch_match more honestly

added dependencies

added an example file with lifting of constants with contravariant and co/contravariant types

merged

make ctxt the first parameter

context/theory parametres tuned

maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types

add induction rule for list_all2

deactivating quickcheck_narrowing if Efficient_Nat theory is loaded

tuned quickcheck's response

more systematic lemma name

adding examples for quickcheck narrowing about partial functions

removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions

HOLCF/ex/Letrec.thy: keep class 'domain' as default sort

more error checking for fixrec

reinstate old functions cfst and csnd as abbreviations

merged

tuned

merged

added a specific tactic and method that deal with partial equivalence relations

use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts

avoid multiple TFF1 declarations

updated TFF1 support

updated Metis to 20110926 version

remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead

add cancellation simprocs for type enat

tuned

increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure

tuned proofs

added lemmas

tuned proof

real is better supported than real_of_nat, use it in the nat => ereal coercion

merged

the note about morphisms moved in the description part

updating documentation about quiet and verbose options in quickcheck

making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples

adding verbose configuration to quickcheck

random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument

the reporting random testing also returns if the counterexample is genuine or potentially spurious

exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly

inverted flag potential to genuine_only in the quickcheck narrowing Haskell code

NEWS

documenting the genuine_only option in quickcheck;

renaming potential flag to genuine_only flag with an inverse semantics

quickcheck narrowing continues searching after found a potentially spurious counterexample

outputing the potentially spurious counterexample and continue search

dynamic genuine_flag in compilation of random and exhaustive

indicating where the restart should occur; making safe_if dynamic

merged

enforce parantheses around SKIP {_}

adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);

merged

remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality

missing dependency

improved var names

invariant holds before loop

caret_range based on BreakIterator, which handles combined unicode characters as well;

misc tuning;

some localization;

eliminated some legacy operations;

more antiquotations;

tuned whitespace;

eliminated some legacy operations;

removed dead code, which has never been active in recorded history;

do not open ML structures;

tuned signature;

hide quickcheck constants Abs_cfun and Rep_cfun, to avoid clash with HOLCF

hiding internal constants and facts more properly

removing catch_match' now that catch_match is polymorphic

adapting exhaustive generators in record package

outputing if counterexample is potentially spurious or not

making catch_match polymorphic

compilations return genuine flag to quickcheck framework

extending quickcheck's result by the genuine flag

reporting random compilation also catches match exceptions internally

the narrowing also indicates if counterexample is potentially spurious

the simple exhaustive compilation also indicates if counterexample is potentially spurious;

quickcheck-random compilation also indicates if the counterexample is potentially spurious or not

changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier

quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception

adding examples for quickcheck-random

removing exception handling now that is caught at some other point; tuned message

quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;

merged

merged IMP/Util into IMP/Vars

use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure

cardinality of sets of lists

do not import examples Probability theory

moved theorems about distribution to the definition; removed oopsed-lemma

rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution

remove duplicate theorem setsum_real_distribution

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

updated Sledgehammer docs with new/renamed options

added "minimize" option for more control over automatic minimization

renamed "slicing" to "slice"

tuning

minor example tweak

renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

updated markup conforming to ML side;

discontinued obsolete datatype "alt_names";

misc tuning;

merged

removed outdated comment moved back and updated (at the direct request of Christian Urban)

more stable introduction of the internally used unknown term

prefer typedef without alternative name;

prefer cpodef without extra definition;

prefer typedef without extra definition and alternative name; tuned proofs;

tuned layout;

tuned header;

updated version information;

removed outdated comment

adding examples for the potential counterexamples in the simple scheme

also potential counterexamples in the simple exhaustive testing in quickcheck

quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned

adding more verbose messages to exhaustive quickcheck

quickcheck narrowing also shows potential counterexamples

adding a exception-safe term reification step in quickcheck; adding examples

quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions

adding parsing of potential configuration to quickcheck command

adding quickcheck's potential configuration

more conventional file name;

merged

updated documentation for the quotient package

merged

alternative names of morphisms in the definition of a quotient type can be specified

adjusting antiquote_setup (cf. d83797ef0d2d)

clarified Time vs. Timing;

separate compilation of PIDE vs. Pure sources, which enables independent Scala library;

clarified modules;

tuned proofs;

rearranged files;

merged

use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)

explicit indication of modules for independent Scala library;

separate module for concrete Isabelle markup;

renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;

tuned signature (according to ML version);

merged

Hide Product_Type.Times - too precious an identifier

more antiquotations;

tuned messages;

avoid stepping outside of context -- plain zero_var_indexes should be sufficient;

increasing timeout to avoid test failures

merged

merged

simplified Collecting1 and renamed: step -> step', step_cs -> step

more antiquotations;

tuned proof;

permissive update for improved "tool compliance"; tuned;

just one data slot per module; tuned;

tuned;

tuned;

more antiquotations;

misc tuning;

refined "literal" document style, with some correspondence to actual text source;

modernized section about congruence rules;

sharing of token source with span source;

memoing of forked proofs;

tuned;

removed obsolete argument (cf. 954e9d6782ea);

merged

removed obsolete uses of Local_Theory.restore -- package composition P1 #> P2 no longer requires them due to 57def0b39696: P2 finds the results of P1 in the auxiliary context

merged

tuned

increased stack limits (again, cf. d9cf3520083c and 77c3e74bd954);

explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;

tuned proofs;

retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;

recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory

in a local context, also the free variable case needs to be analysed default tip

speed-up proof;

more abstract datatype stamp, which avoids pointless allocation of mutable cells;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

simplified -- empty_ss already contains minimal mksimps;

Abstract interpretation is now based uniformly on annotated programs, including a collecting and a small step semantics

tuned;

tuned;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

tuned;

updated according to bdcaa3f3a2f4;

updated proof;

tuned

remove outdated comment

NEWS;

simplified read_instantiate -- no longer need to assign values, since rule attributes are now static;

drop vacuous decls;

tuned;

tuned header;

misspelled name

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

explicit is better than implicit;

eliminated obsolete "standard";

tuned signature;

'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;

updated comment;

more uniform signature;

uniform cert_vars/read_vars;

eliminated dead code;

clarified certify vs. sharing;

tuned;

NEWS;

added ML antiquotation @{attributes};

merged

made SML/NJ happy

simplified Locale.add_thmss, after partial evaluation of attributes;

misc tuning;

tuned;

refined partial evaluation of attributes: avoid duplication of facts for plain declarations; tuned;

discontinued slightly odd write_prv, which would still write .prv files the first time, and deprive add-on tools from date stamp change (cf. 157e74588c49);

do not store vacuous theorem specifications -- relevant for frugal local theory content; tuned;

put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory; tuned;

sequential lemmas to accomodate static rule attributes;

partial evaluation of locale facts leads to static scoping of rule attributes;

tuned message;

gave SML/NJ a chance

more robust options

adding another example for lifting definitions

improving header

more "metis" calls in example

be more silent when auto minimizing

less offensive terminology

more "metis" calls in example

minor textual improvement

pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones

wrap lambdas earlier, to get more control over beta/eta

move eta-contraction to before translation to Metis, to ensure everything stays in sync

avoid that var names get changed by resolution in Metis lambda-lifting

better threading of type encodings between Sledgehammer and "metis"

fixed bugs in lambda-lifting code -- ensure distinct names for variables

protect prefix against variant mutations

example cleanup

example cleanup

don't propagate user-set "type_enc" or "lam_trans" to Metis calls

don't needlessly pass "lam_lifted" option to "metis" call for SMT proof

avoid spurious messages in "lam_lifting" mode

eta-contract to avoid needless "lambda" wrappers

quiet down SMT

more aggressive lambda hiding (if we anyway need to pass an option to Metis)

updated Sledgehammer docs

don't pass "lam_lifted" option to "metis" unless there's a good reason

no needless reconstructors

removed more clutter

removed needless baggage

Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs

merged

Groups.thy: generalize several lemmas from class ab_group_add to class group_add

HOL-Word: removed more duplicate theorems

HOL-Word: removed many duplicate theorems (see NEWS)

Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations

move definitions of bitwise operators into appropriate document section

HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs

HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'

simplify implementation of approx_reorient_simproc

name simp theorems st_0 and st_1

remove redundant simp rules plus_enat_0

eliminated slightly odd Rep' with dynamically-scoped [simplified]; tuned proofs;

partial evaluation in invisible context;

adding a preliminary example to show how the quotient_definition package can be generalized

tuned header

adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition

simplify some proofs

Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead

merged

rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests

remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead

simplify proof of word_of_int; remove several now-unused lemmas about Rep_Integ

retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;

clarified Attrib.partial_evaluation;

tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);

compile

compile

compile

give each time slice its own lambda translation

thread in additional options to minimizer

make metis reconstruction handling more flexible

document metis options better

fixed typo

document "lam_trans" option

nicer bullets

parse lambda translation option in Metis

rename the lambda translation schemes, so that they are understandable out of context

rename configuration option to more reasonable length

continued implementation of lambda-lifting in Metis

disable debugging output

use consts, not frees, for lambda-lifting

started implementing lambda-lifting in Metis

improved generators for rational numbers to generate negative numbers; added examples

tuned

remove one more old-style semicolon

Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs

remove old-style semicolons

avoid theorem references like 'semiring_norm(111)'

merged

merged

Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere

avoid numeral-representation-specific rules in metis proof

merged

remove sorry, otherwise it breaks the testboard

cleaned up float theories; removed duplicate definitions and theorems

enforce quick_and_dirty in Code_Real_Approx_By_Float

some support for partial evaluation of attributed facts;

tuned;

eliminated dead code;

inner syntax positions for string literals;

less confusion subexpression markup;

pass positions for named targets, for formal links in the document model;

simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;

more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);

merged

setting up exhaustive generators which are used for the smart generators

add Code_Real_Approx_By_Float

merged

remove lemma float_remove_real_numeral, which duplicated Float.float_number_of

remove unnecessary number-representation-specific rules from metis calls; speed up another proof

avoid confusing selector output

remove unsound line in Nitpick's "rat" setup

tuned proofs;

merged

removed some old-style semicolons

index markup elements for more efficient cumulate/select operations;

tuned;

tuned markup -- prefer user-perspective;

tuned specifications and proofs;

more precise type;

refined Markup_Tree implementation: stacked markup within each entry; tuned;

tuned signature; express select in terms of cumulate;

tuned signature;

merged

merged

abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite; add tests for abel_cancel simprocs

use simproc_setup for the remaining nat_numeral simprocs

use simproc_setup for more nat_numeral simprocs; add simproc tests

using more conventional names for monad plus operations

more tooltip content;

added markup_cumulate operator;

depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);

tuned;

more abstract Markup_Tree;

prefer statically typed Text.Markup;

discontinued entity text color, notably historic red for classes; tuned entity names;

more scalable Proof_Context.prepare_sorts; reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);

increasing values_timeout to avoid failures of isatest with HOL-IMP

renaming example invocations: tester predicate_compile is renamed to smart_exhaustive

adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;

adding option allow_function_inversion to quickcheck options

more efficient prepare_sorts -- bypass encoded positions;

suppress irrelevant positions;

more generous margin;

pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;

tuned signature;

discontinued unused Thm.compress (again);

renewed prolog-quickcheck

adding some test cases for preprocessing and narrowing

adding a minimalistic preprocessing rewriting common boolean operators; tuned

merged

merged

tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1

use simproc_setup for some nat_numeral simprocs; add simproc tests

add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat.

simultaneous check; tight maxidx;

avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);

clarified singleton_fixate: intersection with supersort is identity, only replace actual type inference parameters; tuned reject_other, after_infer_fixate;

misc tuning and simplification;

misc tuning;

tuned signature; tuned;

quickcheck invocations in mutabelle must not catch codegenerator errors internally

sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;

tuned;

avoid inconsistent sort constraints;

localized Record.decode_type: use standard Proof_Context.get_sort; clarified Record.varifyT: more convential use of maxidx + 1;

tuned signature -- emphasize internal role of these operations;

proper configuration option; tuned;

tuned layout;

more precise messages with the tester's name in quickcheck; tuned

quickcheck fails with code generator errors only if one tester is invoked

removing extra arguments

removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result

tuned

more fragments to export, removed the one from Com

updated functor Named_Thms; updated type attribute;

disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;

entity markup for bound variables;

merged

made SML/NJ happy

adding some documentation about the values command to the isar reference

adding a minimal documentation about the code_pred command to the isar reference

more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);

clarified Local_Defs.export: avoid costly still_fixed test, return all defs;

eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);

tuned;

tuned;

tweaked comment

made SML/NJ happy

merged;

added FIXME comment

avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals

revived Refute in Mutabelle

tuned;

more scalable zero_var_indexes, depending on canonical order within table;

more benchmarks;

try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways

replace higher-order matching against schematic theorem with dedicated reconstruction method

merged

tuned signature -- avoid spurious Thm.mixed_attribute;

discontinued numbered structure indexes (legacy feature);

tuned proofs;

return outcome code, so that it can be picked up by Mutabelle

align columns in output and keep error log around

offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;

clarified attribute "mono_set": pure declaration, proper export in ML;

misc tuning;

made SML/NJ happy;

more millisecond cleanup

updated documentation

try "smt" as a fallback for ATPs if "metis" fails/times out

more detailed preplay output

tuning

tuning

more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;

tuned;

merged

cascading timeouts in minimizer, part 2

tuning

use "Time.time" rather than milliseconds internally

tune: no need for option

cascading timeouts in minimizer

shortcut binary minimization algorithm

speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half

renamed experimental systems

repaired quantification over type variables for non-TFF1/THF encodings

misc tuning and modernization; more antiquotations;

misc tuning and modernization; more antiquotations;

tuned;

some statespace benchmarks;

write changed .prv files only, to avoid writing into src file-space by default;

tuned document; tuned proofs;

more precise dependencies;

inlined antiquotations;

misc tuning and modernization;

optional timing, to avoid redundant allocation of mutable cells;

tuned;

misc tuning;

merged

more use of global operations (see 98ec8b51af9c)

more uniform instT_subst vs. inst_subst: compare variable names only;

tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;

misc tuning and modernization;

some performance tuning via Term_Subst/Same.operation; tuned;

pruned signature;

added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;

more conventional syntax const;

proper syntactic category for abstraction syntax, to avoid low-level exception for malformed "\<integral> x y. f \<partial>M", for example;

merged