src/HOL/Decision_Procs/langford.ML
Sun, 02 Mar 2014 22:37:55 +0100 wenzelm silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
Sun, 02 Mar 2014 22:24:52 +0100 wenzelm tuned whitespace;
Thu, 27 Feb 2014 21:27:58 +0100 wenzelm tuned whitespace;
Sat, 15 Feb 2014 18:48:43 +0100 wenzelm removed dead code;
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, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
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, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
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
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Tue, 25 May 2010 22:21:31 +0200 wenzelm moved ML files where they are actually used;
less more (0) tip