src/HOL/Tools/inductive.ML
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
Tue, 01 Jun 2010 15:38:47 +0200 blanchet removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Mon, 17 May 2010 15:05:32 +0200 wenzelm tuned;
Sun, 16 May 2010 00:02:11 +0200 wenzelm prefer structure Parse_Spec;
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 =)
Tue, 04 May 2010 12:29:22 +0200 berghofe Corrected handling of "for" parameters.
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Wed, 28 Apr 2010 11:26:10 +0200 haftmann fix "fors" for proof of monotonicity
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.
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Sun, 31 Jan 2010 15:22:40 +0100 berghofe merged
Sat, 30 Jan 2010 16:56:28 +0100 berghofe Added "constraints" tag / attribute for specifying the number of equality
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Mon, 30 Nov 2009 08:08:31 +0100 haftmann merged
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Fri, 27 Nov 2009 16:24:31 +0100 berghofe Simplified treatment of monotonicity rules.
Thu, 19 Nov 2009 14:46:33 +0100 wenzelm adapted Local_Theory.define -- eliminated odd thm kind;
Tue, 17 Nov 2009 14:51:57 +0100 wenzelm eliminated slightly odd name space grouping -- now managed by Isar toplevel;
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;
Fri, 13 Nov 2009 17:25:09 +0100 wenzelm eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Tue, 10 Nov 2009 18:32:41 +0100 wenzelm merged
Tue, 10 Nov 2009 13:54:00 +0100 blanchet merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
Thu, 05 Nov 2009 11:58:36 +0100 blanchet merged
Thu, 05 Nov 2009 11:58:07 +0100 blanchet added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
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;
Thu, 05 Nov 2009 22:08:47 +0100 wenzelm adapted LocalTheory.declaration;
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 29 Oct 2009 23:49:55 +0100 wenzelm eliminated some old folds;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Wed, 28 Oct 2009 16:25:27 +0100 wenzelm conceal internal bindings;
Sun, 25 Oct 2009 19:21:34 +0100 wenzelm name space groups are identified by serial, not serial_string;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Thu, 22 Oct 2009 16:52:06 +0200 haftmann arg_types_of auxiliary function; using multiset operations
Wed, 21 Oct 2009 17:34:35 +0200 blanchet renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
Wed, 21 Oct 2009 15:54:01 +0200 haftmann more accurate removal
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Wed, 30 Sep 2009 08:22:07 +0200 haftmann mandatory prefix where appropriate
Wed, 23 Sep 2009 12:03:47 +0200 haftmann stripped legacy ML bindings
Fri, 18 Sep 2009 16:00:56 +0200 haftmann rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
Fri, 18 Sep 2009 09:07:49 +0200 haftmann more antiquotations
Fri, 24 Jul 2009 22:59:08 +0200 wenzelm more antiquotations instead of adhoc ML stuff;
Fri, 24 Jul 2009 18:58:58 +0200 wenzelm renamed functor ProjectRuleFun to Project_Rule;
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
less more (0) -60 tip