2010-01-20 bulwahn 2010-01-20 adopting Sequences
2010-01-20 bulwahn 2010-01-20 added registration of equational theorems from prim_rec and rec_def to Spec_Rules
2010-01-20 bulwahn 2010-01-20 merged
2010-01-18 krauss 2010-01-18 function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
2010-01-20 bulwahn 2010-01-20 merged
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2010-01-22 haftmann 2010-01-22 simplified proofs
2010-01-22 haftmann 2010-01-22 NEWS
2010-01-22 haftmann 2010-01-22 more accurate dependencies
2010-01-22 haftmann 2010-01-22 code literals: distinguish numeral classes by different entries
2010-01-22 haftmann 2010-01-22 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
2010-01-21 haftmann 2010-01-21 merged
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2010-01-16 haftmann 2010-01-16 explicit CONST in translations
2010-01-16 haftmann 2010-01-16 modernized syntax
2010-01-20 blanchet 2010-01-20 fix issues with previous Nitpick change
2010-01-20 blanchet 2010-01-20 merged
2010-01-20 blanchet 2010-01-20 some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"
2010-01-14 blanchet 2010-01-14 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
2010-01-19 hoelzl 2010-01-19 Added transpose_rectangle, when the input list is rectangular.
2010-01-19 hoelzl 2010-01-19 Add transpose to the List-theory.
2010-02-02 wenzelm 2010-02-02 some examples for basic context operations;
2010-02-02 wenzelm 2010-02-02 minimal tuning of this slightly dated material;
2010-02-02 wenzelm 2010-02-02 added Subgoal.FOCUS; misc tuning and clarification;
2010-02-02 wenzelm 2010-02-02 misc tuning and clarification;
2010-02-02 wenzelm 2010-02-02 moved examples to proper place;
2010-02-01 wenzelm 2010-02-01 more details on long names, binding/naming, name space; tuned;
2010-01-31 wenzelm 2010-01-31 Variable.names_of; tuned;
2010-01-31 wenzelm 2010-01-31 more details on Isabelle symbols;
2010-01-29 wenzelm 2010-01-29 theory data example;
2010-01-29 wenzelm 2010-01-29 basic setup for ML examples: tag "mlex";
2010-01-28 wenzelm 2010-01-28 tuned signature;
2010-01-28 wenzelm 2010-01-28 formal markup of type aliases; updated/tuned/clarified contexts; misc tuning and clarification;
2010-01-28 wenzelm 2010-01-28 make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
2010-01-16 wenzelm 2010-01-16 Netbeans Library "Scala-compiler";
2010-01-15 berghofe 2010-01-15 union is an abbreviation for sup.
2010-01-15 berghofe 2010-01-15 merged
2010-01-15 berghofe 2010-01-15 Eliminated is_open option of Rule_Cases.make_nested/make_common; use Rule_Cases.internalize_params to rename parameters instead.
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2010-01-10 berghofe 2010-01-10 Adapted to changes in setup of induct method.
2010-01-10 berghofe 2010-01-10 Expand proofs of induct_atomize'/rulify'.
2010-01-10 berghofe 2010-01-10 Changed case names of converse_rtranclp_induct.
2010-01-10 berghofe 2010-01-10 Injectivity / distinctness theorems are now used to simplify induction rules.
2010-01-10 berghofe 2010-01-10 same_append_eq / append_same_eq are now used for simplifying induction rules.
2010-01-10 berghofe 2010-01-10 Tuned some proofs; nicer case names for some of the induction / cases rules.
2010-01-10 berghofe 2010-01-10 Added setup for simplification of equality constraints in induction rules.
2010-01-10 berghofe 2010-01-10 Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.
2010-01-15 haftmann 2010-01-15 spurious proof failure
2010-01-14 haftmann 2010-01-14 merged
2010-01-14 haftmann 2010-01-14 merged
2010-01-14 haftmann 2010-01-14 dropped unused binding
2010-01-14 haftmann 2010-01-14 dedicated conversions to and from Int
2010-01-14 haftmann 2010-01-14 printing of cases
2010-01-14 haftmann 2010-01-14 tuned for products vs. tupled functions
2010-01-14 haftmann 2010-01-14 added Scala setup
2010-01-14 haftmann 2010-01-14 allow individual printing of numerals during code serialization
2010-01-14 blanchet 2010-01-14 reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
2010-01-14 haftmann 2010-01-14 adjusted to changes in code equation administration
2010-01-13 haftmann 2010-01-13 explicit abstract type of code certificates
2010-01-13 haftmann 2010-01-13 corrected error messages; tuned