merged

tuned

mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties

merged

removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)

removed [trans] concept from basic material

merged

tuned

merged

modernizing predicate_compile_quickcheck

adding depth as an quickcheck configuration

renamed name -> vname

removed some remaining artefacts of ancient SML code generator

NEWS

cleaner LEO-II extensionality step detection

marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs

one more LEO-II failure

merged

merged

hide typedef-generated constants Product_Type.prod and Sum_Type.sum

more uniform SZS status handling

avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"

merged

renamed B to Bc

tuned comment;

proper source positions for @{lemma};

more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

tuned legacy signature;

further cleanup of stats (cf. 97e81a8aa277);

updated keywords;

really document just one code generator;

NEWS

removing old code generator

removing declaration of code_unfold to address the old code generator

removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const

removing documentation about the old code generator

removing old code generator setup for executable sets

removing old code generator setup for efficient natural numbers; cleaned typo

removing old code generator setup for real numbers; tuned

removing old code generator setup for rational numbers; tuned

removing old code generator setup for strings

removing old code generator setup for lists

removing old code generator setup for integers

removing old code generator for inductive predicates

removing quickcheck tester SML-inductive based on the old code generator

removing old code generator setup for inductive sets in the inductive set package

removing old code generator setup of inductive predicates

removing old code generator setup for product types

removing old code generator setup for function types

removing old code generator setup for datatypes

removing old code generator for recursive functions

removing old code generator setup in the HOL theory

removing invocations of the evaluation method based on the old code generator

removing invocations of the old code generator

freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing

gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations

tuned

adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra

mira: collect size of heap images

updated doc related to Satallax

parse Satallax unsat cores

merged

(old) NEWS

moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms

always use sockets on Windows/Cygwin; discontinued special raw_dump facility;

mira configuration: use official polyml 5.4.1 on lxbroy10

added Term.dummy_pattern conveniences;

slightly more standard-conformant XML parsing (see also 94033767ef9b);

tuned proof

tuned type annnotation

hide not_member as also member

misc tuning and modernization;

updated to Scala 2.8.2.final;

prefer recent polyml-5.4.1, but retain potentially fragile polyml-5.2.1 as experimental test;

updated to polyml-5.4.1;

updated to polyml-5.4.1;

merged

monadic bind

moved sublists to More_List.thy

NEWS

more complete stats, including small sessions which provide some clues on main HOL baseline performance;

avoid very specific code equation for card; corrected spelling

bouned transitive closure

moved acyclic predicate up in hierarchy

tuned

modernized definitions

static dummy_task (again) to avoid a few extra allocations;

tuned markup

discontinued obsolete 'types' command;

modernized structure Induct_Tacs;

tuned signature;

misc tuning and clarification;

tuned ML style;

tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;

discontinued obsolete alias structure ProofContext;

separated monotonicity reasoning and defined narrowing with while_option

include no-smlnj targets into library (cf. e54a985daa61);

increasing values_timeout to avoid SML_makeall failures on our current tests

merged

removed obsolete RC tags;

Int.thy: discontinued some legacy theorems

Set.thy: remove redundant [simp] declarations

removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++

tune text for document generation

adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well

adding code equations for cardinality and (reflexive) transitive closure on finite types

adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure

adding lemma to List library for executable equation of the (refl) transitive closure

fixed typos in IMP

added nice interval syntax

Added dependecies

Added Hoare-like Abstract Interpretation

moved IMP/AbsInt stuff into subdirectory Abs_Int_Den

back to post-release mode;

Added tag Isabelle2011-1 for changeset 76fef3e57004

tuned;

updated ISABELLE_HOME_USER;

more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;

Added tag Isabelle2011-1-RC2 for changeset a45121ffcfcb