Quot/Examples/IntEx.thy
Thu, 21 Jan 2010 09:55:05 +0100 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
Thu, 14 Jan 2010 15:25:24 +0100 Cezary Kaliszyk Simplified matches_typ.
Wed, 13 Jan 2010 13:12:04 +0100 Cezary Kaliszyk Removed the 'oops' in IntEx.
Wed, 13 Jan 2010 00:46:31 +0100 Christian Urban tuned
Wed, 13 Jan 2010 00:45:28 +0100 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
Mon, 11 Jan 2010 11:51:19 +0100 Cezary Kaliszyk Fix for testing matching constants in regularize.
Mon, 11 Jan 2010 00:31:29 +0100 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
less more (0) -30 -10 -7 tip