hiding enum

adapting example in Predicate_Compile_Examples

hiding the constants

improving function is_iterable in quickcheck

adding temporary options to the quickcheck examples

adapting the quickcheck examples

adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle

adding code equations for EX1 on finite types

adding code equation for function equality; adding some instantiations for the finite types

adding Enum to HOL-Main image and removing it from HOL-Library

moving Enum theory from HOL/Library to HOL

splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck

adding prototype for finite_type instantiations

adding option finite_types to quickcheck

adding test cases for smallcheck and adding examples where exhaustive testing is more successful

changed old-style quickcheck configurations to new Config.T configurations

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