intelligible errors instead of tactic failures

reenabled yet another example

made new tactic even more robust

reenabled more examples

fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)

reintroduced more examples

improved tactic further

reenabled example

improved new countability tactic

'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems

more robust exception handling

added tests for new 'countable_datatype' proof method

lessen the burden on the caller: sort where necessary in n2m

added compatibility function

added countable tactic for new-style datatypes

tuning

registered 'typerep' as countable again

moved old datatype material around

removed vacuous theorem references

commented out failing tactic (now that 'typerep' is defined using the new package

tuned imports

use 'datatype_new'

use 'datatype_new' in 'Main'

take out 'x = C' of the simplifier for unit types

giving up calling 'datatype_compat' in a locale -- causes trouble with extensions

ported 'Statespace' to support new datatypes as well

use 'datatype_new' in Quickcheck examples

more compatibility functions

codatatypes are not datatypes

ported Quickcheck to support new datatypes better

removed more slow Refute tests

tuned Refute example

Some work on the new waldmeister integration

merged

replay Z3 rewrite steps that lift if-then-else expressions

test discriminators/selectors in BNF regression suite

merge

made SML/NJ happier

tuning

silenced nonexhaustive primrec warnings

more convenient printing of real numbers after evaluation

avoid more 'bad background theory' issues

ported TFL to mixture of old and new datatypes

drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'

ported to use new-style datatypes * * * compile

ported Refute to use new datatypes when possible

renamed BNF theories

renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'

added primrec compatibility function

more work on compatibility interfaces

added compatibility examples/tests

implemented compatibility definition of datatype

implemented compatibility interpretation

compile

compile

tuning

compile

more compatibility between old- and new-style datatypes

added theory-based getters for convenience

made transfer functions slightly more general

tuned signatures

tuning

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

tuned structure inclusion

took out legacy material from 'HOL/Library/Library.thy'

removed commented out parts

tuned whitespace

document 'set_transfer'

generate 'set_transfer' for BNFs

document 'rel_transfer'

generate 'rel_transfer' for BNFs

document 'map_transfer'

note 'map_transfer' more often

separated listsum material

restored generic value slot, retaining default behaviour and separate approximate command

convenient printing of (- 1 :: integer) after code evaluation

inlined unused definition

add simp rules for divisions of numerals in floor and ceiling.

document 'disc_transfer'

generate 'disc_transfer' for (co)datatypes

document 'case_transfer'

generate 'case_transfer' for (co)datatypes

renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods

reworked unskolemization for SPASS

clarified docs

gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)

prefer '0.2 ms' to '249 \<mu>s'

use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)

fixed second computations

merged minimize and auto_minimize

pass options to remote Vampire

removed show stuttering

generate 'thesis' variable in Sledgehammer Isar proofs

show microseconds as well (useful when playing with Isar proofs)

tuned message

made trace more informative when minimization is enabled

took out one more occurrence of 'PolyML.makestring'

try 'skolem' method first for Z3

tuned tracing output (indirectly)

going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.

moved skolem method

added 'skolem' method, esp. for 'obtain's generated from Z3 proofs

tuned method description

three-line 'obtain' format for generated Isar proofs

tuned;

more liberal embedded "text", which includes cartouches;

intern xthm only once;

tuned terminology

moved new para to right section of NEWS

minor NEWS fix

keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof

added 'OLD_' prefix in front of old solvers

updated NEWS

renamed new SMT module from 'SMT2' to 'SMT'

updated NEWS

prefixed all old SMT commands, attributes, etc., with 'old_'

add 'old_' prefix to SMT file names; add 'Old_' to ML module names;

renaming theory 'Old_SMT'

moved old setup for SMT out

moved old 'smt' method out of 'Main'

reintroduced two-line-per-inference Isar proof format

removed needless, and for (newer versions of?) Haskell problematic code equations

removed obsolete RC tags;

merged

Added tag Isabelle2014 for changeset 8f4a332500e4

merged

more explicit Method.modifier with reported position;

tuned signature -- prefer quasi-abstract Symbol_Pos.source;

added ML antiquotation @{source} for Symbol_Pos.source;

tuned signature;

removed not so interesting 'set_empty'

avoid 'PolyML.makestring'

introduce real_of typeclass for real :: 'a => real

added lemmas

better linarith support for floor, ceiling, natfloor, and natceiling

add testing framework for generated code

correct code equation for term_of on integer

merged

add code equation for term_of on integer

added lemmas contributed by Rene Thiemann

attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";

tuned whitespace;

clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;

merged

made SML/NJ happy;

clarified Method.section: explicit declaration with static closure;

tuned signature -- define some elementary operations earlier;

discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;

tuned;

tuned;

tuned;

generic euclidean algorithm (due to Manuel Eberl)

integrated appendix theory into main theory; tuned ML

dropped dead file

fix tactic failure with rel_induct0 minimal example: datatype_new 'a A1 = A1 nat and 'a A2 = A2 'a

added jdk-8u20 (inactive);

proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;

support for declaration within token source;

more uniform data slot;

default command position is only valid for default text chunk (amending dcb758188aa6);

tuned -- more total;

tuned;

support for nested Token.src within Token.T; tuned signature;

tuned signature -- moved type src to Token, without aliases;

merged

clarified modules;

added PARALLEL_ALLGOALS convenience;

just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);

tuned signature;

more compact datatypes;

tuned;

clarifed Method.evaluate: turn text into semantic method (like Basic);

simplified type Proof.method;

more general dummy: may contain "parked arguments", for example;

document 'ctr_transfer'

generate 'ctr_transfer' for (co)datatypes

rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup

Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)

reduced dependency on 'Datatype' theory and ML module

removed Z3 3.2, now superseded by Z3 4.3

avoid old 'smt' method in examples

robustified tactics

tuning

don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set

documented slight incompatibility in NEWS

removed junk

updated docs

set attributes on 'set_cases' theorem

cleaned up derivation of 'sset_induct'

tuning

added collection theorem for consistency and convenience

reordered some (co)datatype property names for more consistency

document 'map_cong_simp'

generate 'map_cong_simp' for BNFs

merged

merged;

Added tag Isabelle2014-RC4 for changeset 113b43b84412

updated to jdk-7u67;

postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;

explicit system message for protocol failure -- show on Syslog panel instead of Raw Output; more robust crash recovery: warning could crash again;

added option editor_syslog_limit;

tuned;

updated to cygwin-20140813 -- some version after 1.7.31-3;

document 'inj_map_strong'

generate 'inj_map_strong' for BNFs

note 'inj_map' more often

generate property 'rel_mono_strong' for BNFs

renamed 'rel_mono_strong' to 'rel_mono_strong0'

use 'image_mset' as BNF map function

made SML/NJ happy;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems; modernized setup;

updated to named_theorems; modernized module name and setup;

clarified order of rules;

updated to named_theorems; modernized setup; tuned;

updated to named_theorems;

clarified order of arith rules;

clarified order of rules for match_tac/resolve_tac;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

modernized module name and setup;

updated syntax for localized commands;

updated documentation concerning 'named_theorems';

prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;

more informative Token.Name with history of morphisms; tuned signature;

merged

more informative Token.Fact: retain name of dynamic fact (without selection);

localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;

T1 font encoding with searchable underscore (requires proper cm-super fonts);

prefer high-level change of \isabellestyle;

tuned;

tuned;

tuned signature;

localized method definitions (see also f14c1248d064);