adding temporary function test_test_small to Quickcheck

added useful function map_context_result to signature

moving the error handling to the right scope in smallvalue_generators

removing clone from function package and using the clean interface from Function_Relation instead

adding function generation to SmallCheck; activating exhaustive search space testing

adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict

generalized ensure_random_datatype to ensure_sort_datatype

renaming quickcheck generator code to random

ported sledgehammer_tactic to current development version

adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test

adding files to use sledgehammer as a tactic for non-interactive use

adding birthday paradoxon from some abandoned drawer

adding extensional function spaces to the FuncSet library theory

tuned

tuned

updated explode vs. raw_explode;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

total Symbol.explode (cf. 1050315f6ee2);

do not export Thy_Load.required, to avoid confusion about the interface;

merged

declare adm_chfin [simp]

add lemma cont_fun; remove unused lemma monofun_app

accumulated NEWS updates for HOLCF

section -> subsection

add lemma adm_prod_case

merged

First-order pattern matching: catch a rogue exception (differing numbers of arguments)

eval simp rules for predicate type, simplify primitive proofs

generalized type

made smlnj happy

merged

proper qualification needed due to shadowing on theory merge

more appropriate name for property

mapper for sum type

mapper for option type

mapper for list type; map_pair replaces prod_fun

map_pair replaces prod_fun

mapper for mulitset type

mapper for mapping type

mapper for fset type

mapper for dlist type

map_fun combinator in theory Fun

some updates after 2 years of Mercurial usage;

mention Sledgehammer with SMT

enabled SMT solver in Sledgehammer by default

merged

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;

tuned message;

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);

more reasonably defaults for typical laptops (2 GB RAM, 2 cores); enforce -server JVM if possible (NB: default JRE on Windows lacks that);

added forall2 predicate lifter

merged

merged

renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

honour timeouts which are not rounded to full seconds

better error message

better error message

merged

cosmetics

interpret SMT_Failure.Solver_Crashed correctly

turn on Sledgehammer verbosity so we can track down crashes

pick up SMT solver crashes and report them to the user/Mirabelle if desired

merged

only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers

trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)

merged

ignoring the constant STR in the predicate compiler

non-executable source files;

eliminated old-style sed in favour of builtin regex matching;

more robust treatment of spaces in file names;

tuned error messages;

merged

re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)

re-generalized type of prod_rel (accident from 2989f9f3aa10)

formal dependency on b2i files

merged

check the return code of the SMT solver and raise an exception if the prover failed

updated README;

tuned;

cover 'write' as primitive proof command;

clarified interact/print state: proof commands are treated as in TTY mode to get full response;

somewhat adhoc replacement for 'thus' and 'hence'; complete words as short as 2 characters, e.g. "Un";

always print state of proof commands (notably "qed" etc.);

simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

tuned message;

proper escape in regex;

report malformed symbols;

qualified Symbol_Pos.symbol;

total Symbol.source;

eliminated slightly odd pervasive Symbol_Pos.symbol;

treat Unicode "replacement character" (i.e. decoding error) is malformed;