ML signature interface

stub for Isar command interface

module for functorial mappers

merged

require the b2i file ending in the boogie_open command (for consistency with the theory header)

use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)

keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)

add lemmas about powerdomains

declare {upper,lower,convex}_pd_induct as default induction rules

rename 'repdef' to 'domaindef'

refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;

less parentheses, cf. Session.welcome;

avoid spam;

more robust determination of java executable;