src/HOL/Nominal/nominal_fresh_fun.ML
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Thu, 11 Sep 2014 21:11:03 +0200 blanchet fixed some spelling mistakes
Sat, 22 Mar 2014 18:16:54 +0100 wenzelm more antiquotations;
Thu, 20 Mar 2014 19:58:33 +0100 wenzelm more standard method_setup;
Thu, 06 Mar 2014 12:43:29 +0100 wenzelm more rigid type_name demands, based on educated guesses about the tools involved here;
Thu, 06 Mar 2014 12:10:19 +0100 wenzelm tuned signature -- more uniform check_type_name/read_type_name;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 12:24:43 +0200 wenzelm proper proof context;
Wed, 21 Mar 2012 11:00:34 +0100 wenzelm prefer explicitly qualified exception List.Empty;
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Sat, 14 May 2011 16:27:47 +0200 wenzelm modernized structure Rule_Insts;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Wed, 12 Jan 2011 15:07:29 +0100 wenzelm avoid catch-all exception handler, presumably TERM was meant here;
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;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Tue, 09 Mar 2010 14:55:25 +0100 wenzelm tuned -- eliminated Sign.intern_sort;
Thu, 25 Feb 2010 22:06:43 +0100 wenzelm clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
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;
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Tue, 20 Oct 2009 23:25:04 +0200 wenzelm eliminated THENL -- use THEN RANGE;
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;
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;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Mon, 29 Sep 2008 11:46:47 +0200 wenzelm handle _ should be avoided (spurious Interrupt will spoil the game);
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Thu, 12 Jun 2008 23:12:54 +0200 wenzelm use regular error function;
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;
Sat, 08 Sep 2007 18:30:02 +0200 urbanc some cleaning up
Tue, 14 Aug 2007 23:22:51 +0200 wenzelm avoid low-level tsig;
Wed, 13 Jun 2007 11:16:24 +0200 narboux generate_fresh works even if there is no free variable in the goal
Thu, 24 May 2007 14:04:06 +0200 narboux fix a bug : the semantics of no_asm was the opposite
Thu, 24 May 2007 12:00:47 +0200 narboux add an option in fresh_fun_simp to prevent rewriting in assumptions
Mon, 21 May 2007 19:14:12 +0200 narboux search bottom up to get the inner fresh fun
Mon, 21 May 2007 16:19:56 +0200 narboux change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
Wed, 25 Apr 2007 15:38:56 +0200 narboux fix sml compilation
Tue, 24 Apr 2007 18:06:04 +0200 narboux update fresh_fun_simp for debugging purposes
Tue, 24 Apr 2007 14:01:23 +0200 narboux adds op in front of an infix to fix SML compilation
Fri, 20 Apr 2007 14:30:35 +0200 narboux modify fresh_fun_simp to ease debugging
Thu, 19 Apr 2007 16:27:53 +0200 narboux add a tactic to generate fresh names
less more (0) tip