more foundational definition for predicate even

New example Bubblesort

formally completeted set of experimental static evaluation functions

merged

afford slightly bigger JVM stack (see also f7ba30a816b9);

prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);

prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;

proper @{cite} with bibtex entry (unchecked comment);

fix document generation in Code_Test

merged

eliminated some exotic combinators;

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

tuned;

tuned;

clarified messages depending on options; misc tuning and simplification;

simplified "sos" method;

tuned signature; tuned whitespace;

tuned spelling; tuned whitespace;

add Linear Temporal Logic on Streams

move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS

proper bibliography;

more antiquotations;

more bibtex entries; more antiquotations;

more antiquotations;

tuned whitespace;

more antiquotations;

clarified whitespace;

more cartouches;

more cartouches;

more cartouches;

merged

more cartouches; more antiquotations;

more cartouches; more antiquotations;

more symbols;

more cartouches;

added update_cartouches tool;

removed pointless regexp flags;

fix document generation for HOL-Probability

move Stream theory from Datatype_Examples to Library

add Giry monad

tuned

improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;

merged

tuned spaces

avoid creating needless skolemization steps for SPASS

get rid of 'individual' type in DFG proofs

slightly nicer names

strengthened 'moura' method

improved unskolemization of SPASS problems

more total parser;

more defensive error handling -- token marker must not crash;

merged

documentation of @{cite} and cite_macro;

completion for bibtex entries;

more accurate item name, depending on kind; tuned;

back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;

tuned signature;

add measure space for (coinductive) streams

add type for probability mass functions, i.e. discrete probability distribution

refactor 'map_sel_thms' and 'set_sel_thms'

rename 'xtor_rel_thms' to 'xtor_rels'

rename 'xtor_set_thmss' to 'xtor_setss'

rename 'xtor_map_thms' to 'xtor_maps'

rename one of the two 'rel_eq_thms' to 'rel_code_thms'

rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'

rename 'dtor_set_induct_thms' to 'dtor_set_inducts'

rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'

rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'

add 'set_inducts' to 'fp_sugar'

add 'common_set_inducts' to 'fp_sugar'

add 'rel_co_inducts' to 'fp_sugar'

add 'common_rel_co_induct' to 'fp_sugar'

add 'co_rec_transfers' to 'fp_sugar'

add 'co_rec_disc_iffs' to 'fp_sugar'

add 'disc_transfers' to 'fp_sugar'

add 'case_transfers' to 'fp_sugar'

add 'ctr_transfers' to 'fp_sugar'

add 'set_cases' to 'fp_sugar'

add 'set_intros' to 'fp_sugar'

add 'set_sels' to 'fp_sugar'

add 'set_thms' to 'fp_sugar'

add 'rel_cases' to 'fp_sugar'

add 'rel_intros' to 'fp_sugar'

add 'rel_sels' to 'fp_sugar'

add 'map_sels' to 'fp_sugar'

add 'map_disc_iffs' to 'fp_sugar'

code preprocessor tracing also for function transformers

basic support for fully static evaluator generation without dynamic compiler invocation

split dynamic from static context

more refs;

prefer @{cite} antiquotation;

prefer @{cite} antiquotation;

prefer @{cite} antiquotation;

prefer @{cite} antiquotation;

NEWS;

more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;

clarified modules;

clarified modules;

clarified modules;

clarified modules;

citation tooltip/hyperlink based on open buffers with .bib files;

bibtex support in ML: document antiquotation @{cite} with markup;

maintain Document_Model.bibtex_entries; clarified Chunk predicates;

more advanced NEWS tree structure and folding;

merged;

NEWS;

tuned output;

proper treatment of @comment (amending 402a8e8107a7);

mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);

more total chunk_line: recovery via ignored_line;

more explicit comments;

clarified nesting of delimiters; tuned;

fields are case-insensitive;

clarified nesting of delimiters;

more explicit chunk name;

clarified Chunk -- avoid ooddities;

support for bibtex token markup; more robust ML token marker: no_context; tuned signature;

more explicit item kind; clarified recover_delimited: skip to next @; support for line context parsing; tuned signature;

strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;

SideKick parser for bibtex entries; tuned signature;

more buffer.isEditable checks;

context menu for bibtex entries;

some support for bibtex files;

tuned

tuned

accomplish potentially case-insenstive file systems for Scala

tuned

merge

more precise lemma insertion

insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem

avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition

eliminate duplicate hypotheses (which can arise due to (un)clausification)

formal lcm definition for polynomials

moved lemmas out of Int.thy which have nothing to do with int

redundant: dropped

tuned Heap_Monad.successE

documentation

fixed a few mistakes in the documentation

tuning

'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3

actually finish after closing, e.g. relevant for consecutive (**)(**);

tuned

tuned;

tuned

don't call 'hd' on a possibly empty list

proper types for applied variables, for typed formats (TFF0, DFG)

don't affect other subgoals with 'auto' in one-liner proofs

tuned output in case of one-liner failure

updated docs with two provers: veriT and Zipperposition

give more facts to veriT -- it seems to be able to cope with them

use native encoding with Vampire -- modern versions handle types better than the old ones

always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')

correct inlining in veriT's subproofs.

repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'

tuning

tuning

keep rules with no premises in Isar proofs from veriT

correct indexing in the presence of lambda-lifting

merged

tuned

merge

support hypotheses with schematics in Isar proofs

tuned

simplified and repaired veriT index handling code

made 'moura' tactic more powerful

fixed wrong optimization (wrong because it may affect the sequent's conclusion)

merge

added option to get cleaner SPASS proofs

parse back type of SPASS proof variables

make sure no '__' suffixes make it until Isar proof

rename skolem symbols in the negative case as well

reintroduced 'rel_cases' in docs

added options to Mirabelle

tuning

faster machine for slow/bulky polyml-5.3.0 tests (notably HOL-Proofs);

pro-forma support for polyml-5.5.3 (presently SVN 1960);

corrected white-space accident

tuned

moved to HOL and generalized

merged

proper range for Antiq tokens; more detailed parse trees; report sub-expressions;

support for sub-expression markup;

tuned message;

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar with empty substructures

add attribute 'case_names' to 'set_case'

make 'case_transfer' tactic more robust

more correct precedence of do-notation

merged

save image as PNG or PDF; more robust error dialog;

support for PNG output;

more isatests (on lxbroy4);

document 'corec_transfer'

generate 'corec_transfer' for codatatypes

document 'rec_transfer'

generate 'rec_transfer' for datatypes

generate 'dtor_corec_transfer' for codatatypes

generate 'ctor_rec_transfer' for datatypes

goal generation for xtor_co_rec_transfer

commented out some tests that require external tools (e.g. ghc)

added useful options to CVC4

subscribe for isatest

even more deads go to the end (continuation of e3a01b73579f)

added function size1

added lemmas

tuned

avoid type variable name clash

tuning

made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow

improved 'bnf' parser

updated SMT certificates

allow homogeneous nesting for SMT (co)datatypes

interleave (co)datatypes in the right order w.r.t. dependencies

rule out nested (co)recursion for SMT (co)datatypes

gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'

tuning

simpler proof

added nice standard syntax

clarified timeout for isatest;

merged

discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation;

added csdp-6.x for proof method (sos csdp);

examples for local CSDP executable;

clarified SOS tool setup vs. examples;

make 'set_induct0' tactic more robust w.r.t multiple arguments constructors

merged

clarified ISABELLE_POLYML; added some isatests -- ISABELLE_SCALA still inactive due to problems with case-insensible file-system;

drop workaround addressed by d0d3c30806b4

renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;

more standard Isabelle/ML operations;

tuned;

explicit separation of signed and unsigned numerals using existing lexical categories num and xnum

corrected slip in documentation

Removed double space

Changed proof method to auto for custom Waldmeister lemma

Minor fixes in ATP_Waldmeister

Made encoded type for apply less restrictive

Updated fix_name function

Added support for partial function application

Improved equality handling in skolemization

Re-added hypothesis argument to problem generation

always annotate potentially polymorphic Haskell numerals

tuned

simplified and tuned using signed_string_of_int

tuned data structure

tuning

documented limitations

more honest 'primcorec' -- don't parse a theorem name that is then ignored

tuning

added a few tests for 'old_datatype'

reintroduced old setup for size of basic types

keep obsolete interpretations in Main, to avoid merge trouble

made new 'primrec' bootstrapping-capable

tuning

tuning

typo

regression tests for n2m

merged

add lemma

tuned imports

removed debugging junk

help AFP entry 'Free-Groups' to compile

reintroduced an instantiation of 'size' for 'numerals'

use selector

moved old 'size' generator together with 'old_datatype'

moved datatype realizer to 'old_datatype' and colleagues

careful with op = in n2m (actually by Dmitriy Traytel)

fixed attribute name in docs (thanks to Andreas Lochbihler)

updated NEWS

moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again

increased 'HOL-Proofs' timeout

made 'mk_pointfree' work again in local theories

fixed authorship

product over monoids for lists

renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming

more meaningful record tests

updated SMT certificates

tuning

take out selectors for records -- for derived records, these don't quite have the right type

register Isabelle selectors as SMT selectors when possible

added codatatype support for CVC4

added interface for CVC4 extensions

avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')

tweaked compatibility layer

avoid clash with Quickcheck's generated 'random_xxx' function

added missing 'restore' in 'transfer' plugin

syntactic check to determine when to prove 'nested_size_o_map'

support (finite values of) codatatypes in Quickcheck

tuned fact visibility

register 'prod' and 'sum' as datatypes, to allow N2M through them

took out 'old_datatype' examples -- those just cause timeouts in Isatests

added 'extraction' plugins -- this might help 'HOL-Proofs'

added lemma

add target language evaluators for the value command; drop obsolete command eval_term

tuning

refactoring

tuning

set 'mono' attribute on 'rel_mono'

'code' is needed for extraction datatype

tuning

removed accidental '@{print}'

tuning

more hints on how to port 'size'

tuned definition of 'size' function to get nicer properties

tuning

document size difference

generate 'code' attribute only if 'code' plugin is enabled

disable datatype 'plugins' for internal types

ported Imperative HOL to new datatypes

imported patch phantoms

enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines

new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead

run larger nominal examples only 'ISABELLE_FULL_TEST'

refactor repeated terms in a single variable

make 'ctr_transfer' tactic more robust

make 'rel_sel' and 'map_sel' tactics more robust

Changing the way the dependencies are managed.

correction in the thf0 parser ("(=)" found in a Satallax proof).

merge

fixed spellings

NEWS

abstract product over monoid for lists

use proto_base_sort uniformly

fixed some spelling mistakes

tuned comment

more porting to new datatypes

tuning terminology

compile

renamed example theory for consistency

updated ROOT

tuned documentation

updated news

renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')

move datatype benchmarks

use new datatypes for benchmarks

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'

tuning

fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'

tuning

fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'

speed up old Nominal by killing type variables

took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)

more docs

new deads go to the end

comment

more material on lists

explicit check phase to guide type inference of class expression towards one single type variable

tuned

dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns

tuning

proper checks -- the calls data structure may contain spurious entries

avoid exception

avoid internal fact

restored old case names

compile

avoid duplicate case names

nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')

preserve case names in '(co)induct' theorems generated by prim(co)rec'

hide DEADID/ID theorems

tuning

more canonical (and correct) local theory threading

removed 'datatype_compat's that are no longer needed

documented extraction plugin

made realizer more robust in the face of nesting through functions

removed debugging junk

renamed ML file and module

made datatype realizer plugin work for new-style datatypes with no nesting

ported HOL-Proofs-Lambda to new datatypes

ported HOL-Proofs-Extraction to new datatypes

made SML/NJ happier

more porting to new datatypes

tuned IArray code generator w.r.t. map rel set

ported Nitpick_Examples to new datatypes

set 'fundef_cong' attribute also for (co)datatypes with no live type variables

ported IArray to new datatypes

prevent infinite loop when type variables are of a non-'type' sort

tuned code

ported MicroJava to new datatypes

rename_tac'd scrips