keep variables bound

remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem

merged

infer variances of user-given mapper operation; proper thm storing

code eqn for slice was missing; redefined splice with fun

move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain

merged

typedef (open) unit

add bind_bind rules for powerdomains

merged

emerging Isar command interface

fixed typo

updated keywords

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;

init_component: require absolute path (when invoked by user scripts);

more explicit explanation of init_component shell function;

paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;