src/HOL/Tools/inductive_set.ML
Wed, 01 Jan 2014 14:29:22 +0100 wenzelm clarified simplifier context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 08 Jan 2013 17:10:06 +0100 wenzelm more tolerant set/pred rule declaration to improve "tool compliance", notably for "context assumes";
Wed, 12 Sep 2012 14:46:13 +0200 wenzelm removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
Wed, 05 Sep 2012 19:51:00 +0200 wenzelm discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names;
Wed, 07 Mar 2012 16:13:49 +0100 berghofe to_pred/set attributes now properly handle variables of type "... => T set"
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Sat, 24 Dec 2011 16:14:58 +0100 haftmann treatment of type constructor `set`
Mon, 07 Nov 2011 14:23:50 +0100 wenzelm clarified attribute "mono_set": pure declaration, proper export in ML;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Wed, 19 Oct 2011 08:37:23 +0200 bulwahn removing old code generator setup for inductive sets in the inductive set package
Mon, 01 Aug 2011 12:08:53 +0200 nipkow infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
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