src/HOL/Fact.thy
Tue, 17 Jan 2012 16:30:54 +0100 huffman factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
Mon, 19 Dec 2011 14:41:08 +0100 noschinl add lemmas
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Tue, 19 Oct 2010 12:26:38 +0200 bulwahn added some facts about factorial and dvd, div and mod
Mon, 08 Mar 2010 09:38:58 +0100 haftmann transfer: avoid camel case
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 29 Oct 2009 11:41:37 +0100 haftmann moved algebraic classes to Ring_and_Field
Thu, 10 Sep 2009 15:26:51 +0200 haftmann obey underscore naming convention
Fri, 17 Jul 2009 13:12:18 -0400 avigad Changed fact_Suc_nat back to fact_Suc
Tue, 14 Jul 2009 17:17:37 +0200 berghofe Use term antiquotation to refer to constant names in subsection title.
Fri, 10 Jul 2009 10:45:30 -0400 avigad Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 24 Feb 2009 11:12:58 -0800 huffman make more proofs work whether or not One_nat_def is a simp rule
Mon, 23 Feb 2009 07:58:13 -0800 huffman change imports to move Fact.thy outside Plain
Fri, 30 Jan 2009 12:48:56 +0000 chaieb moved upwards in thy graph, real related theorems moved to Transcendental.thy
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip