src/Sequents/simpdata.ML
Wed, 11 Jan 2012 16:25:34 +0100 wenzelm more qualified names;
Mon, 28 Nov 2011 17:05:41 +0100 wenzelm avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
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;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Tue, 17 Aug 2010 19:36:39 +0200 haftmann more antiquotations
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
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;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 23 Jul 2009 23:12:21 +0200 wenzelm more @{theory} antiquotations;
less more (0) -15 tip