src/HOL/Nominal/nominal_primrec.ML
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
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;
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all;
Fri, 02 Dec 2011 14:54:25 +0100 wenzelm more antiquotations;
Fri, 02 Dec 2011 13:51:36 +0100 wenzelm do not open ML structures;
Sat, 19 Nov 2011 21:18:38 +0100 wenzelm added ML antiquotation @{attributes};
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sun, 16 May 2010 00:02:11 +0200 wenzelm prefer structure Parse_Spec;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Wed, 10 Feb 2010 17:05:18 +0100 berghofe Fixed bug in code for guessing the name of the variable representing the freshness context.
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
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 17:25:09 +0100 wenzelm eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Sun, 25 Oct 2009 19:21:34 +0100 wenzelm name space groups are identified by serial, not serial_string;
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 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
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, 25 Jul 2009 18:55:30 +0200 wenzelm fixed Method.Basic;
Sat, 25 Jul 2009 18:04:15 +0200 wenzelm Method.Basic: no position;
Fri, 03 Jul 2009 23:29:03 +0200 haftmann nominal.ML is nominal_datatype.ML
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
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
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Thu, 12 Mar 2009 21:55:02 +0100 wenzelm simplified preparation and outer parsing of specification;
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 15:49:39 +0100 blanchet Fix parentheses.
Wed, 04 Mar 2009 15:32:57 +0100 blanchet Added "nitpick_const_simp" attribute to Nominal primrec.
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, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Sat, 13 Dec 2008 13:24:45 +0100 berghofe Modified nominal_primrec to make it work with local theories, unified syntax
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 29 Mar 2008 13:03:07 +0100 wenzelm eliminated quiete_mode ref (unused);
Thu, 06 Dec 2007 15:10:09 +0100 haftmann added new primrec package
Mon, 08 Oct 2007 18:13:05 +0200 wenzelm turned keywords invariant/freshness_context into reserved indentifiers;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Thu, 30 Aug 2007 22:35:34 +0200 wenzelm replaced ProofContext.infer_types by general Syntax.check_terms;
less more (0) -60 tip