src/HOL/Quotient.thy
Thu, 22 Apr 2010 11:55:19 +0200 Cezary Kaliszyk fun_rel introduction and list_rel elimination for quotient package
Tue, 20 Apr 2010 14:56:20 +0200 Cezary Kaliszyk respectfullness and preservation of function composition
Tue, 13 Apr 2010 11:40:03 +0200 Cezary Kaliszyk add If respectfullness and preservation to Quotient package database
Mon, 12 Apr 2010 13:19:28 +0200 Cezary Kaliszyk Changed the type of Quot_True, so that it is an HOL constant.
Wed, 17 Mar 2010 19:37:44 +0100 blanchet renamed "ATP_Linkup" theory to "Sledgehammer"
Mon, 22 Feb 2010 21:48:20 -0800 huffman proper header and subsection headings
Fri, 19 Feb 2010 17:37:33 +0100 Cezary Kaliszyk quote the constant and theorem name with @{text}
Fri, 19 Feb 2010 13:54:19 +0100 Cezary Kaliszyk Initial version of HOL quotient package.
less more (0) tip