QuotMain.thy
Thu, 24 Sep 2009 13:32:52 +0200 Cezary Kaliszyk Minor cleanup
Thu, 24 Sep 2009 11:38:20 +0200 Cezary Kaliszyk Found the source for the exception and added a handle for it.
Thu, 24 Sep 2009 09:09:46 +0200 Cezary Kaliszyk Make the tactic use Trueprop_cong and atomize.
Wed, 23 Sep 2009 16:57:56 +0200 Cezary Kaliszyk Proper code for getting the prop out of the theorem.
Wed, 23 Sep 2009 16:44:56 +0200 Cezary Kaliszyk Using "atomize" the versions with arbitrary Trueprops can be proven.
Tue, 22 Sep 2009 17:39:52 +0200 Cezary Kaliszyk Proper definition of CARD and some properties of it.
Tue, 22 Sep 2009 09:42:27 +0200 Christian Urban some comments
Mon, 21 Sep 2009 18:18:29 +0200 Christian Urban merged
Mon, 21 Sep 2009 18:18:01 +0200 Christian Urban slight tuning
Mon, 21 Sep 2009 16:45:44 +0200 Cezary Kaliszyk The tactic with REPEAT, CHANGED and a proper simpset.
Mon, 21 Sep 2009 10:53:01 +0200 Cezary Kaliszyk Merged with my changes from the morning:
Sun, 20 Sep 2009 05:48:49 +0100 Ning some more beautification
Sun, 20 Sep 2009 05:18:36 +0100 Ning beautification of some proofs
Fri, 18 Sep 2009 17:30:33 +0200 Cezary Kaliszyk Added more useful quotient facts.
less more (0) -14 tip