correctly hiding facts of Lazy_Sequence

corrected and simplified Spec_Rules registration in the Recdef package

merged

adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps

adopting Sequences

added registration of equational theorems from prim_rec and rec_def to Spec_Rules

merged

function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations

merged

refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck

simplified proofs

NEWS

more accurate dependencies

code literals: distinguish numeral classes by different entries

cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation

merged

dropped some old primrecs and some constdefs

explicit CONST in translations

modernized syntax

fix issues with previous Nitpick change

merged

some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"

removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value

Added transpose_rectangle, when the input list is rectangular.

Add transpose to the List-theory.

some examples for basic context operations;

minimal tuning of this slightly dated material;

added Subgoal.FOCUS; misc tuning and clarification;

misc tuning and clarification;

moved examples to proper place;

more details on long names, binding/naming, name space; tuned;

Variable.names_of; tuned;

more details on Isabelle symbols;

theory data example;

basic setup for ML examples: tag "mlex";

tuned signature;

formal markup of type aliases; updated/tuned/clarified contexts; misc tuning and clarification;

make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);

Netbeans Library "Scala-compiler";

union is an abbreviation for sup.

merged

Eliminated is_open option of Rule_Cases.make_nested/make_common; use Rule_Cases.internalize_params to rename parameters instead.

Adapted to changes in induct method.

Adapted to changes in setup of induct method.

Expand proofs of induct_atomize'/rulify'.

Changed case names of converse_rtranclp_induct.

Injectivity / distinctness theorems are now used to simplify induction rules.

same_append_eq / append_same_eq are now used for simplifying induction rules.

Tuned some proofs; nicer case names for some of the induction / cases rules.

Added setup for simplification of equality constraints in induction rules.

Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.

spurious proof failure

merged

merged

dropped unused binding

dedicated conversions to and from Int

printing of cases

tuned for products vs. tupled functions

added Scala setup

allow individual printing of numerals during code serialization