src/HOL/Nominal/nominal_atoms.ML
Tue, 10 Jan 2012 23:58:10 +0100 berghofe Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete
Sat, 24 Dec 2011 16:14:58 +0100 haftmann treatment of type constructor `set`
Tue, 13 Dec 2011 23:23:51 +0100 wenzelm 'datatype' specifications allow explicit sort constraints;
Wed, 30 Nov 2011 23:30:08 +0100 wenzelm discontinued obsolete datatype "alt_names";
Wed, 12 Oct 2011 22:48:23 +0200 wenzelm modernized structure Induct_Tacs;
Sat, 03 Sep 2011 23:59:36 +0200 haftmann tuned specifications
Sat, 03 Sep 2011 17:32:34 +0200 haftmann assert Pure equations for theorem references; tuned
Sat, 15 Jan 2011 12:38:56 +0100 berghofe Finally removed old primrec package, since Primrec.add_primrec_global
Wed, 15 Dec 2010 15:01:34 +0100 wenzelm eliminated dead code;
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;
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Thu, 10 Jun 2010 12:24:03 +0200 haftmann tuned quotes, antiquotations and whitespace
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Tue, 23 Jun 2009 15:32:34 +0200 haftmann add_datatypes does not yield particular rules any longer
Tue, 23 Jun 2009 14:50:34 +0200 haftmann add_datatype interface yields type names and less rules
Sun, 21 Jun 2009 08:38:58 +0200 haftmann simplified names of common datatype types
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Wed, 17 Jun 2009 08:13:05 +0200 haftmann datatype packages: record datatype_config for configuration flags; less verbose signatures
Thu, 07 May 2009 12:02:16 +0200 haftmann explicit type_name antiquotations
Thu, 19 Mar 2009 22:05:00 +0100 wenzelm proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
Sat, 07 Mar 2009 22:17:25 +0100 wenzelm more uniform handling of binding in packages;
Wed, 04 Mar 2009 10:47:20 +0100 nipkow Made Option a separate theory and renamed option_map to Option.map
Wed, 25 Feb 2009 11:02:25 +0100 berghofe Added equivariance lemmas for fresh_star.
Wed, 21 Jan 2009 18:27:43 +0100 haftmann binding replaces bstring
Tue, 16 Dec 2008 20:32:41 +0000 Christian Urban changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 10 Nov 2008 17:34:26 +0100 berghofe Some more functions for accessing information about atoms.
Fri, 26 Sep 2008 14:52:27 +0200 berghofe Added some more theorems to NominalData.
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Wed, 27 Aug 2008 04:47:30 +0200 urbanc added equivariance lemmas for ex1 and the
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Mon, 30 Jun 2008 14:06:44 +0200 urbanc added facts to lemma swap_simps and tuned lemma calc_atms
Sat, 14 Jun 2008 23:20:09 +0200 wenzelm InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
Tue, 10 Jun 2008 19:15:21 +0200 wenzelm InductTacs.case_tac with proper context and proper declaration of local variable;
Tue, 10 Jun 2008 15:31:04 +0200 haftmann polished interface of datatype package
Mon, 09 Jun 2008 17:07:08 +0200 wenzelm adapted case_tac/induct_tac;
Wed, 07 May 2008 10:59:35 +0200 berghofe - Deleted arity proofs for set
Fri, 02 May 2008 22:43:14 +0200 urbanc added more infrastructure for fresh_star
Sat, 29 Mar 2008 19:14:06 +0100 wenzelm eliminated non-linear access to thy1 and thy12c;
Tue, 25 Mar 2008 21:28:39 +0100 wenzelm removed redundant axiomatizations of XXX_infinite (fact already proven);
Thu, 20 Mar 2008 00:20:44 +0100 wenzelm simplified get_thm(s): back to plain name argument;
Wed, 19 Mar 2008 22:28:08 +0100 wenzelm auxiliary dynamic_thm(s) for fact lookup;
Mon, 18 Feb 2008 03:12:08 +0100 urbanc added eqvt-flag to subseteq-lemma
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Thu, 06 Dec 2007 15:10:09 +0100 haftmann added new primrec package
Wed, 05 Dec 2007 14:16:05 +0100 haftmann map_product and fold_product
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;
Sun, 23 Sep 2007 22:10:27 +0200 urbanc changed the representation of atoms to datatypes over nats
Thu, 13 Sep 2007 18:08:08 +0200 berghofe Added equivariance lemmas for induct_forall.
Wed, 05 Sep 2007 15:46:32 +0200 urbanc modified proofs so that they are not using claset()
Fri, 10 Aug 2007 17:04:24 +0200 haftmann ClassPackage renamed to Class
Thu, 09 Aug 2007 15:52:42 +0200 haftmann re-eliminated Option.thy
Tue, 07 Aug 2007 09:38:44 +0200 haftmann split off theory Option for benefit of code generator
Sat, 21 Jul 2007 23:25:00 +0200 wenzelm tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
Thu, 31 May 2007 14:47:20 +0200 urbanc introduced symmetric variants of the lemmas for alpha-equivalence
less more (0) -100 -60 tip