2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-12 bulwahn 2010-03-12 adding Spec_Rules to definitional package inductive and inductive_set
2010-03-08 berghofe 2010-03-08 Added inducts field to inductive_result.
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-01-30 berghofe 2010-01-30 Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.
2010-01-14 haftmann 2010-01-14 dropped unused binding
2009-11-19 wenzelm 2009-11-19 adapted Local_Theory.define -- eliminated odd thm kind;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-13 wenzelm 2009-11-13 inductive: eliminated obsolete kind;
2009-11-12 wenzelm 2009-11-12 eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 tuned;
2009-11-05 wenzelm 2009-11-05 proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context; tuned signature; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-08-10 haftmann 2009-08-10 merged
2009-07-30 haftmann 2009-07-30 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-08-04 bulwahn 2009-08-04 removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
2009-07-29 haftmann 2009-07-29 cleaned up abstract tuple operations and named them consistently
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"