src/HOL/NSA/transfer.ML
Mon, 23 Mar 2015 19:05:14 +0100 haftmann distributivity of partial minus establishes desired properties of dvd in semirings
Fri, 06 Mar 2015 23:57:01 +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;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
Wed, 29 Oct 2014 17:01:44 +0100 wenzelm modernized setup;
Sat, 22 Mar 2014 20:42:16 +0100 wenzelm more antiquotations;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Wed, 04 Apr 2012 09:00:10 +0200 huffman rename ML structure to avoid shadowing earlier name
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Thu, 03 Jul 2008 17:47:22 +0200 huffman move nonstandard analysis theories to NSA directory
less more (0) tip