src/HOL/Decision_Procs/ferrack_tac.ML
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Fri, 06 Mar 2015 23:33:25 +0100 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;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Fri, 14 Feb 2014 22:03:48 +0100 wenzelm proper signature;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Tue, 27 Mar 2012 14:49:56 +0200 huffman remove redundant lemmas
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sun, 27 Nov 2011 23:10:19 +0100 wenzelm more antiquotations;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Wed, 12 May 2010 12:09:28 +0200 haftmann modernized specifications; tuned reification
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Fri, 19 Feb 2010 16:45:21 +0100 wenzelm local Simplifier.context;
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;
Mon, 19 Oct 2009 23:02:56 +0200 wenzelm always qualify NJ's old List.foldl/foldr in Isabelle/ML;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 24 Jun 2009 09:41:14 +0200 nipkow corrected and unified thm names
Sat, 30 May 2009 13:42:40 +0200 wenzelm proper signature constraint;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 11 Mar 2009 10:58:18 +0100 hoelzl Updated paths in Decision_Procs comments and NEWS
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 17:05:18 +0100 nipkow removed and renamed redundant lemmas
Sat, 21 Feb 2009 09:58:26 +0100 nipkow removed redundant thms
Tue, 17 Feb 2009 18:48:17 +0100 nipkow Cleaned up IntDiv and removed subsumed lemmas.
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
less more (0) tip