FSet.thy
Mon, 23 Nov 2009 23:09:03 +0100 Christian Urban fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Mon, 23 Nov 2009 21:56:30 +0100 Cezary Kaliszyk Another not-typechecking regularized term.
Mon, 23 Nov 2009 21:48:44 +0100 Cezary Kaliszyk domain_type in regularizing equality
Mon, 23 Nov 2009 21:12:16 +0100 Cezary Kaliszyk More theorems lifted in the goal-directed way.
Mon, 23 Nov 2009 14:16:41 +0100 Cezary Kaliszyk Move atomize_goal to QuotMain
Mon, 23 Nov 2009 14:05:02 +0100 Cezary Kaliszyk Removed second implementation of Regularize/Inject from FSet.
Mon, 23 Nov 2009 13:46:14 +0100 Cezary Kaliszyk New repabs behaves the same way as old one.
less more (0) -30 -10 -7 tip