Tue, 08 May 2012 14:35:13 +0200 | bulwahn | defining and proving Executable_Relation with lift_definition and transfer | changeset | files |
Tue, 08 May 2012 14:31:03 +0200 | bulwahn | specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer | changeset | files |
Mon, 07 May 2012 14:50:49 +0200 | blanchet | prevent spurious timeouts | changeset | files |
Mon, 07 May 2012 12:20:55 +0200 | blanchet | added "try0" tool to Mirabelle | changeset | files |
Mon, 07 May 2012 12:20:55 +0200 | blanchet | use latest E (1.5) | changeset | files |
Fri, 04 May 2012 17:12:37 +0200 | huffman | lifting package produces abs_eq_iff rules for total quotients | changeset | files |
Fri, 04 May 2012 11:08:31 +0200 | bulwahn | using the new transfer method to obtain abstract properties of RBT trees | changeset | files |