2010-11-18 wenzelm 2010-11-18 some updates after 2 years of Mercurial usage;
2010-11-18 blanchet 2010-11-18 mention Sledgehammer with SMT
2010-11-18 blanchet 2010-11-18 enabled SMT solver in Sledgehammer by default
2010-11-18 haftmann 2010-11-18 merged
2010-11-18 haftmann 2010-11-18 keep variables bound
2010-11-18 blanchet 2010-11-18 remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
2010-11-17 haftmann 2010-11-17 merged
2010-11-17 haftmann 2010-11-17 infer variances of user-given mapper operation; proper thm storing
2010-11-17 nipkow 2010-11-17 code eqn for slice was missing; redefined splice with fun
2010-11-17 huffman 2010-11-17 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
2010-11-17 huffman 2010-11-17 merged
2010-11-16 huffman 2010-11-16 typedef (open) unit
2010-11-16 huffman 2010-11-16 add bind_bind rules for powerdomains
2010-11-17 wenzelm 2010-11-17 merged
2010-11-17 haftmann 2010-11-17 emerging Isar command interface
2010-11-17 haftmann 2010-11-17 fixed typo
2010-11-17 haftmann 2010-11-17 updated keywords
2010-11-17 haftmann 2010-11-17 ML signature interface
2010-11-17 haftmann 2010-11-17 stub for Isar command interface
2010-11-17 haftmann 2010-11-17 module for functorial mappers
2010-11-17 wenzelm 2010-11-17 merged
2010-11-17 boehmes 2010-11-17 require the b2i file ending in the boogie_open command (for consistency with the theory header)
2010-11-17 boehmes 2010-11-17 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)
2010-11-17 boehmes 2010-11-17 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-16 huffman 2010-11-16 add lemmas about powerdomains
2010-11-16 huffman 2010-11-16 declare {upper,lower,convex}_pd_induct as default induction rules
2010-11-16 huffman 2010-11-16 rename 'repdef' to 'domaindef'
2010-11-17 wenzelm 2010-11-17 refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
2010-11-17 wenzelm 2010-11-17 less parentheses, cf. Session.welcome;
2010-11-16 wenzelm 2010-11-16 avoid spam;
2010-11-16 wenzelm 2010-11-16 more robust determination of java executable;
2010-11-16 wenzelm 2010-11-16 init_component: require absolute path (when invoked by user scripts);
2010-11-16 wenzelm 2010-11-16 more explicit explanation of init_component shell function;
2010-11-16 wenzelm 2010-11-16 paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
2010-11-16 wenzelm 2010-11-16 tuned message;
2010-11-16 wenzelm 2010-11-16 post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
2010-11-16 wenzelm 2010-11-16 more reasonably defaults for typical laptops (2 GB RAM, 2 cores); enforce -server JVM if possible (NB: default JRE on Windows lacks that);
2010-11-16 haftmann 2010-11-16 added forall2 predicate lifter
2010-11-15 wenzelm 2010-11-15 merged
2010-11-15 boehmes 2010-11-15 merged
2010-11-15 boehmes 2010-11-15 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-15 boehmes 2010-11-15 honour timeouts which are not rounded to full seconds
2010-11-15 blanchet 2010-11-15 better error message
2010-11-15 blanchet 2010-11-15 better error message
2010-11-15 wenzelm 2010-11-15 merged
2010-11-15 blanchet 2010-11-15 cosmetics
2010-11-15 blanchet 2010-11-15 interpret SMT_Failure.Solver_Crashed correctly
2010-11-15 blanchet 2010-11-15 turn on Sledgehammer verbosity so we can track down crashes
2010-11-15 blanchet 2010-11-15 pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-11-15 boehmes 2010-11-15 merged
2010-11-15 boehmes 2010-11-15 only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
2010-11-15 boehmes 2010-11-15 trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
2010-11-15 bulwahn 2010-11-15 merged
2010-11-15 bulwahn 2010-11-15 ignoring the constant STR in the predicate compiler
2010-11-15 wenzelm 2010-11-15 non-executable source files;
2010-11-15 wenzelm 2010-11-15 eliminated old-style sed in favour of builtin regex matching;
2010-11-15 wenzelm 2010-11-15 more robust treatment of spaces in file names;
2010-11-15 wenzelm 2010-11-15 tuned error messages;
2010-11-15 wenzelm 2010-11-15 merged
2010-11-15 haftmann 2010-11-15 re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)