Quot/Examples/FSet3.thy
2010-01-13 Christian Urban merged
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 Cezary Kaliszyk Change OO to OOO in FSet3.
2010-01-10 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"
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples.
2010-01-08 Cezary Kaliszyk Experimients with fconcat_insert
2010-01-08 Cezary Kaliszyk Proved concat_empty.
less more (0) -10 -7 tip