src/HOL/Tools/inductive_set.ML
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Mon, 23 Aug 2010 16:47:57 +0200 bulwahn introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
Tue, 20 Jul 2010 23:09:49 +0200 wenzelm discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
Wed, 07 Jul 2010 08:25:21 +0200 bulwahn added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Thu, 10 Jun 2010 12:24:02 +0200 haftmann moved inductive_codegen to place where product type is available; tuned structure name
Wed, 26 May 2010 16:05:25 +0200 haftmann dropped legacy theorem bindings
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Wed, 05 May 2010 18:25:34 +0200 haftmann 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 =)
Fri, 12 Mar 2010 12:14:31 +0100 bulwahn adding Spec_Rules to definitional package inductive and inductive_set
Mon, 08 Mar 2010 15:00:34 +0100 berghofe Added inducts field to inductive_result.
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Sat, 30 Jan 2010 16:56:28 +0100 berghofe Added "constraints" tag / attribute for specifying the number of equality
Thu, 14 Jan 2010 17:54:55 +0100 haftmann dropped unused binding
Thu, 19 Nov 2009 14:46:33 +0100 wenzelm adapted Local_Theory.define -- eliminated odd thm kind;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
Fri, 13 Nov 2009 19:57:46 +0100 wenzelm inductive: eliminated obsolete kind;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 05 Nov 2009 23:59:23 +0100 wenzelm tuned;
Thu, 05 Nov 2009 22:59:57 +0100 wenzelm proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Wed, 28 Oct 2009 16:25:27 +0100 wenzelm conceal internal bindings;
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Sat, 19 Sep 2009 07:38:03 +0200 haftmann inter and union are mere abbreviations for inf and sup
Fri, 18 Sep 2009 09:07:50 +0200 haftmann tuned const_name antiquotations
Mon, 10 Aug 2009 10:25:00 +0200 haftmann merged
Thu, 30 Jul 2009 15:20:57 +0200 haftmann path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
Tue, 04 Aug 2009 08:34:56 +0200 bulwahn removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis
Wed, 29 Jul 2009 16:48:34 +0200 haftmann cleaned up abstract tuple operations and named them consistently
Wed, 22 Jul 2009 14:20:32 +0200 haftmann set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
less more (0) tip