src/HOL/Nominal/nominal_permeq.ML
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 23 Feb 2018 19:25:37 +0100 wenzelm added HOLogic.mk_obj_eq convenience and eliminated some clones;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Sun, 26 Jul 2015 20:56:44 +0200 wenzelm updated to infer_instantiate;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Tue, 02 Jun 2015 09:40:04 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Wed, 09 Apr 2014 12:28:24 +0200 wenzelm more standard names;
Wed, 09 Apr 2014 12:22:57 +0200 wenzelm proper context for print_tac;
Sat, 22 Mar 2014 18:16:54 +0100 wenzelm more antiquotations;
Thu, 20 Mar 2014 19:58:33 +0100 wenzelm more standard method_setup;
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
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
less more (0) -60 tip