print case syntax depending on "show_cases" configuration option;

merged

redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min

remove some uses of Int.succ and Int.pred

removed unused lemmas

remove redundant syntax declaration

use 'induct arbitrary' instead of 'rule_format' attribute

declare simp rules immediately, instead of using 'declare' commands

declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin

be explicit about Finite_Set.fold

dropped fact whose names clash with corresponding facts on canonical fold

prefer canonical fold on lists

be explicit about Finite_Set.fold

incorporated More_Set and More_List into the Main body -- to be consolidated later

moved theorem requiring multisets from More_List to Multiset

NEWS: unavoidable fact renames

dropped disfruitful `constant signatures`

moved various set operations to theory Set (resp. Product_Type)

dropped Executable_Set wrapper theory

updated certificate

NEWS: `set` is now a proper type constructor

dropped references to obsolete facts `mem_def` and `Collect_def`

dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`

adjusted to set/pred distinction by means of type constructor `set`

treatment of type constructor `set`

executable intervals

`set` is now a proper type constructor

tuned layout

reduced to a compatibility layer

added setup for executable code

moved `sublists` to theory Enum

commented out examples which choke on strict set/pred distinction

explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`

adjusted to set/pred distinction by means of type constructor `set`

dropped references to obsolete fact `mem_def`

dropped obsolete lemma member_set

dropped obsolete code equation for Id

tuned proofs

generalized type signature to permit overloading on `set`

added monad instance for `set`

enum type class instance for `set`; dropped misfitting code lemma for trancl

finite type class instance for `set`

treatment of type constructor `set`

lattice type class instances for `set`; added code lemma for Set.bind

`set` is now a proper type constructor; added operation for set monad

simplify some proofs

remove redundant lemma word_sub_def

add lemmas bin_cat_zero and bin_split_zero

more uses of 'induct arbitrary'

use 'induct arbitrary' instead of universal quantifiers

remove two conflicting simp rules for 'number_of (number_of _)' pattern

add lemma bin_nth_minus1

removed killed encoding from example

updated docs

killed "guard@?" encodings -- they were found to be unsound

extend previous optimizations to guard-based encodings

treat polymorphic constructors specially in @? encodings

tuning

no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")

added some basic documentation about method induction_schema extracted from old NEWS

adding documentation about the quickcheck_generator command in the IsarRef

extending quickcheck example

NEWS

quickcheck_generator command also creates random generators

don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers

one more SPASS identifier

tuning

merged

meaningful error message on failing merges of coercion tables

add simp rules for enat and ereal

add lemmas

add lemmas

weaken preconditions on lemmas

add lemmas

removing some debug output in quotient_definition

adding quickcheck generators in some HOL-Library theories

adding quickcheck generator for distinct lists; adding examples

added keywords

quickcheck generators for abstract types; tuned

exporting instantiation functions in quickcheck for their usage in abstract generators

generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;

tuned

tuned

ensure TPTP FOF/TFF/THF formulas are close

tuned

merged

added old chestnut

isarfied proof; add log to DERIV_intros

tendsto lemmas for ln and powr

tuned settings;

updated jedit_build component;

updated version information;

patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);

eliminated Drule.export_without_context which is not really required here;

tuned signature;

enforce short hostname on all platforms (especially macbroy2);

clarified modules that contribute to datatype package;

tuned signature;

merged

merged

improved indexed complete lattice

more elementary defs;

eliminated old-fashioned Global_Theory.add_thms(s);

prefer sorting from Scala library;

prefer Name.context operations;

tuned;

clarified modules that contribute to datatype package;

tuned signature;

merged;

tuned;

add complementary lemmas for {min,max}_least

add lemmas about limits

clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

separate rep_datatype.ML; tuned signature;

misc tuning and simplification;

more stats;

made SML/NJ happier

merged

tuned

hiding the precious name map_entry in AList_Impl