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;