tuned size function generation

tuning

introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

tuned ctr_sugar database handling

tuned BNF database handling

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