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;