2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22 boehmes 2010-01-22 merged
2010-01-22 boehmes 2010-01-22 support skolem constant for extensional arrays in Z3 proofs
2010-01-22 boehmes 2010-01-22 drop underscores at end of names coming from Boogie
2010-01-22 bulwahn 2010-01-22 merged
2010-01-22 bulwahn 2010-01-22 correctly hiding facts of Lazy_Sequence
2010-01-21 bulwahn 2010-01-21 corrected and simplified Spec_Rules registration in the Recdef package
2010-01-21 bulwahn 2010-01-21 merged
2010-01-21 bulwahn 2010-01-21 adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
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