src/HOL/Nominal/nominal_permeq.ML
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 04 Sep 2011 09:28:15 +0200 haftmann tuned
Sat, 03 Sep 2011 15:09:51 -0700 huffman merged
Sat, 03 Sep 2011 14:52:40 -0700 huffman modify nominal packages to better respect set/pred distinction
Sat, 03 Sep 2011 17:32:34 +0200 haftmann assert Pure equations for theorem references; tuned
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
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;
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, 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
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
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;
Wed, 13 Jan 2010 00:08:56 +0100 wenzelm added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
Tue, 10 Nov 2009 18:11:23 +0100 wenzelm eliminated some unused/obsolete Args.bang_facts;
Tue, 27 Oct 2009 22:55:27 +0100 wenzelm Datatype.read_typ: standard argument order;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 28 Sep 2009 22:47:34 +0200 wenzelm moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
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;
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
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;
Mon, 22 Sep 2008 19:46:24 +0200 urbanc made the perm_simp tactic to understand options such as (no_asm)
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Wed, 07 May 2008 10:57:19 +0200 berghofe Adapted to encoding of sets as predicates
Thu, 20 Mar 2008 00:20:44 +0100 wenzelm simplified get_thm(s): back to plain name argument;
Wed, 19 Mar 2008 22:28:17 +0100 wenzelm auxiliary dynamic_thm(s) for fact lookup;
Mon, 28 Jan 2008 18:17:42 +0100 berghofe Cleaned up simproc code.
Thu, 13 Sep 2007 23:58:38 +0200 urbanc some cleaning up to do with contexts
Sun, 02 Sep 2007 12:34:20 +0200 urbanc made theorem-references safe
Thu, 26 Apr 2007 14:24:08 +0200 wenzelm eliminated unnamed infixes, tuned syntax;
Fri, 13 Apr 2007 09:23:35 +0200 narboux debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
Sat, 07 Apr 2007 11:36:35 +0200 urbanc tuned slightly the previous commit
Sat, 07 Apr 2007 11:05:25 +0200 narboux perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
Wed, 04 Apr 2007 20:22:32 +0200 narboux make fresh_guess fail if it does not solve the subgoal
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Tue, 03 Apr 2007 17:05:52 +0200 narboux remove the lemma swap_fun which was not needed
Mon, 02 Apr 2007 23:24:52 +0200 narboux rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
Wed, 28 Mar 2007 18:25:23 +0200 urbanc the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
Tue, 06 Mar 2007 15:28:22 +0100 urbanc major update of the nominal package; there is now an infrastructure
Wed, 07 Feb 2007 17:51:38 +0100 berghofe Adapted to changes in Finite_Set theory.
Wed, 06 Dec 2006 01:12:36 +0100 wenzelm removed legacy ML bindings;
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Fri, 20 Oct 2006 17:07:26 +0200 haftmann slight cleanup
Wed, 04 Oct 2006 14:17:38 +0200 haftmann insert replacing ins ins_int ins_string
Tue, 29 Aug 2006 21:43:34 +0200 urbanc added a FIXME-comment
Wed, 02 Aug 2006 22:26:41 +0200 wenzelm normalized Proof.context/method type aliases;
Tue, 04 Jul 2006 17:26:02 +0200 urbanc added simplification rules to the fresh_guess tactic
Tue, 04 Jul 2006 15:26:56 +0200 berghofe - put declarations inside a structure (NominalPermeq)
Mon, 12 Jun 2006 20:32:33 +0200 urbanc added lemma fresh_unit to Nominal.thy
Mon, 12 Jun 2006 18:17:21 +0200 berghofe Added fresh_guess_tac.
Fri, 28 Apr 2006 15:54:34 +0200 berghofe Renamed "nominal" theory to "Nominal".
Thu, 27 Apr 2006 01:41:30 +0200 urbanc isar-keywords.el
Thu, 06 Apr 2006 17:29:40 +0200 urbanc modified the perm_compose rule such that it
Wed, 01 Mar 2006 18:26:20 +0100 urbanc fixed a problem where a permutation is not analysed
Wed, 01 Mar 2006 10:27:01 +0100 urbanc made some small tunings in the decision-procedure
less more (0) -60 tip