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

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

document new experimental provers

added remote iProver(-Eq) for experimentation

merged

ex/Tree23.thy: automate proof of gfull_add

ex/Tree23.thy: simplify proof of bal_del0

ex/Tree23.thy: simplify proof of bal_add0

ex/Tree23.thy: simpler definition of ordered-ness predicate

ex/Tree23.thy: prove that deletion preserves balance

more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);

more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;

tuned whitespace;

tuned signature;

tuned signature -- canonical argument order;

tuned -- Variable.declare_term is already part of Variable.auto_fixes;

ex/Tree23.thy: prove that insertion preserves tree balance and order

more IMP fragments

string -> vname

JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.

more IMP text fragments

moved latex generation for HOL-IMP out of distribution

renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)

merged

more robust, declarative and unsurprising computation of types in the quotient type definition

improve handling of bound type variables (esp. for TFF1)

improved TFF1 output

clarified signature

tuned

tuned

even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);

removed obsolete argument (cf. aa35859c8741);

removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]

extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'

merged

remove unused function

also export DFG formats

always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions

added DFG unsorted support (like in the old days)

gracefully do nothing if the SPASS input file is already in DFG format

added sorted DFG output for coming version of SPASS

specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9

check "sound" flag before doing something unsound...

uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);

tuned;

more accurate class constraints on cancellation simproc patterns

tuned;

tuned Named_Thms: proper binding;

refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;

more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

slightly more explicit/syntactic modelling of morphisms;

correct import path

allow to build Probability and MV-Analysis with one ROOT.ML

removing dead code

ex/Simproc_Tests.thy: remove duplicate simprocs

use simproc_setup for cancellation simprocs, to get proper name bindings

tuned;

eliminated aliases of standard functions;

more standard attribute setup;

localized quotient data;

simplified/standardized signatures;

tuned signature;

uses IMP and hence requires its tex setup

merged

tuned text

respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception

respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access

respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access

merged

fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

more robust ML pretty printing (cf. b6c527c64789);

tuned;

renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library

tuned text

tuned names to avoid shadowing

merge Gcd/GCD and Lcm/LCM

clarify types of terms: use proper set type

instance bool :: linorder

removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

fixed typo

latex output not needed because errors manifest themselves earlier

some text on inner-syntax;

renamed in ASM

tuned order of eqns

tuned

script for exporting filtered IMP files as tar.gz

removed Norbert's email from isatest (bounces)

class Lexicon as abstract datatype;

more private stuff;

class Text.Edit as abstract datatype;

class Time as abstract datatype;

class Volatile as abstract datatype;

merged

added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file

experimental support for Scala 2.9.1.final;

class Path as abstract datatype;

class Counter as abstract datatype;

discontinued redundant ASCII syntax;

modernized specifications;

proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views); clarified Text.Range apartness, with try_restrict and try_join operations; private Perspective constructor to ensure abstract datatype integrity;

merged

tuned

merged

replacing metis proofs with facts xt1 by new proof with more readable names

more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies

disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction

NEWS

updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

removing redundant attribute code_inline in the code generator

tuned;

tuned;

improving mutabelle script again after missing some changes in f4896c792316

correcting code_prolog

merged

add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML

merged

tuned

mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties

merged

removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)

removed [trans] concept from basic material

merged

tuned

merged

modernizing predicate_compile_quickcheck

adding depth as an quickcheck configuration

renamed name -> vname

removed some remaining artefacts of ancient SML code generator

NEWS

cleaner LEO-II extensionality step detection

marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs

one more LEO-II failure

merged

merged

hide typedef-generated constants Product_Type.prod and Sum_Type.sum

more uniform SZS status handling

avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"

merged

renamed B to Bc

tuned comment;

proper source positions for @{lemma};

more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

tuned legacy signature;

further cleanup of stats (cf. 97e81a8aa277);

updated keywords;

really document just one code generator;

NEWS

removing old code generator

removing declaration of code_unfold to address the old code generator

removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const

removing documentation about the old code generator

removing old code generator setup for executable sets

removing old code generator setup for efficient natural numbers; cleaned typo

removing old code generator setup for real numbers; tuned

removing old code generator setup for rational numbers; tuned

removing old code generator setup for strings

removing old code generator setup for lists

removing old code generator setup for integers

removing old code generator for inductive predicates

removing quickcheck tester SML-inductive based on the old code generator

removing old code generator setup for inductive sets in the inductive set package

removing old code generator setup of inductive predicates

removing old code generator setup for product types

removing old code generator setup for function types

removing old code generator setup for datatypes

removing old code generator for recursive functions

removing old code generator setup in the HOL theory

removing invocations of the evaluation method based on the old code generator

removing invocations of the old code generator

freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing

gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations

tuned

adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra

mira: collect size of heap images

updated doc related to Satallax

parse Satallax unsat cores

merged

(old) NEWS

moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms

always use sockets on Windows/Cygwin; discontinued special raw_dump facility;

mira configuration: use official polyml 5.4.1 on lxbroy10

added Term.dummy_pattern conveniences;

slightly more standard-conformant XML parsing (see also 94033767ef9b);

tuned proof

tuned type annnotation

hide not_member as also member

misc tuning and modernization;

updated to Scala 2.8.2.final;

prefer recent polyml-5.4.1, but retain potentially fragile polyml-5.2.1 as experimental test;

updated to polyml-5.4.1;

updated to polyml-5.4.1;

merged

monadic bind

moved sublists to More_List.thy

NEWS

more complete stats, including small sessions which provide some clues on main HOL baseline performance;

avoid very specific code equation for card; corrected spelling

bouned transitive closure

moved acyclic predicate up in hierarchy

tuned

modernized definitions

static dummy_task (again) to avoid a few extra allocations;

tuned markup

discontinued obsolete 'types' command;

modernized structure Induct_Tacs;

tuned signature;

misc tuning and clarification;

tuned ML style;

tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;

discontinued obsolete alias structure ProofContext;

separated monotonicity reasoning and defined narrowing with while_option

include no-smlnj targets into library (cf. e54a985daa61);

increasing values_timeout to avoid SML_makeall failures on our current tests

merged

removed obsolete RC tags;

Int.thy: discontinued some legacy theorems

Set.thy: remove redundant [simp] declarations

removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++

tune text for document generation

adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well

adding code equations for cardinality and (reflexive) transitive closure on finite types

adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure

adding lemma to List library for executable equation of the (refl) transitive closure