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