src/HOL/Nominal/nominal_primrec.ML
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
less more (0) -15 tip