src/HOL/Nominal/nominal_inductive.ML
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Sat, 14 Jan 2012 20:05:58 +0100 wenzelm renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
Tue, 13 Sep 2011 07:56:46 +0200 haftmann tuned
Sat, 10 Sep 2011 19:44:41 +0200 haftmann more modularization
Sat, 03 Sep 2011 23:59:36 +0200 haftmann tuned specifications
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
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
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;
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
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, 27 Apr 2010 21:34:22 +0200 wenzelm really minimize sorts after certification -- looks like this is intended here;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Fri, 20 Nov 2009 00:20:32 +0100 Christian Urban use of thm-antiquotation
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 17:25:09 +0100 wenzelm eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Sun, 26 Jul 2009 18:57:11 +0200 wenzelm SUBPROOF/Obtain.result: named params;
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;
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Fri, 03 Jul 2009 23:29:03 +0200 haftmann nominal.ML is nominal_datatype.ML
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Mon, 18 May 2009 09:48:06 +0200 haftmann introduced Thm.generatedK
Sat, 16 May 2009 20:17:59 +0200 bulwahn added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
Wed, 11 Mar 2009 15:42:19 +0100 wenzelm explicit Binding.qualified_name -- prevents implicitly qualified bstring;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Wed, 25 Feb 2009 11:05:06 +0100 berghofe nominal_inductive and equivariance now work on local_theory.
Wed, 21 Jan 2009 18:27:43 +0100 haftmann binding replaces bstring
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm eliminated OldTerm.(add_)term_consts;
Wed, 31 Dec 2008 20:31:36 +0100 wenzelm eliminated OldTerm.add_term_free_names;
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Wed, 13 Aug 2008 03:00:33 +0200 berghofe Changed proof of strong induction rule to avoid infinite loop
Mon, 04 Aug 2008 18:56:22 +0200 berghofe - corrected bogus comment for function inst_conj_all
Thu, 03 Jul 2008 00:54:45 +0200 berghofe Rewrote code to use swap_simps rather than calc_atm (which tends to
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Wed, 25 Jun 2008 14:54:45 +0200 berghofe - Equivariance simpset used in proofs of strong induction and inversion
Mon, 16 Jun 2008 17:54:39 +0200 wenzelm allE_Nil: only one copy, proven in regular theory source;
Wed, 11 Jun 2008 18:02:00 +0200 wenzelm Drule.read_instantiate;
less more (0) -60 tip