2010-11-30 haftmann [Tue, 30 Nov 2010 17:22:59 +0100] rev 40825
adaptions to changes in Equiv_Relation.thy
src/HOL/Induct/QuoDataType.thy

2010-11-30 haftmann [Tue, 30 Nov 2010 17:19:11 +0100] rev 40824
adapted fragile proof
src/HOL/ZF/Games.thy

2010-11-30 haftmann [Tue, 30 Nov 2010 17:19:11 +0100] rev 40823
adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
src/HOL/Quotient_Examples/Quotient_Message.thy

2010-11-30 haftmann [Tue, 30 Nov 2010 17:19:11 +0100] rev 40822
adaptions to changes in Equiv_Relation.thy
src/HOL/Induct/QuoNestedDataType.thy src/HOL/Library/Fraction_Field.thy src/HOL/Quotient_Examples/FSet.thy src/HOL/ex/Dedekind_Real.thy

2010-11-30 haftmann [Tue, 30 Nov 2010 15:58:21 +0100] rev 40821
merged
NEWS

2010-11-30 haftmann [Tue, 30 Nov 2010 15:58:09 +0100] rev 40820
more systematic and compact proofs on type relation operators using natural deduction rules
src/HOL/Library/Quotient_List.thy src/HOL/Library/Quotient_Option.thy src/HOL/Library/Quotient_Product.thy src/HOL/Library/Quotient_Sum.thy

2010-11-30 haftmann [Tue, 30 Nov 2010 15:58:09 +0100] rev 40819
adapted proofs to slightly changed definitions of congruent(2)
src/HOL/Int.thy src/HOL/Rat.thy

2010-11-29 haftmann [Mon, 29 Nov 2010 22:47:55 +0100] rev 40818
reorienting iff in Quotient_rel prevents simplifier looping;
lemma QuotientI;
tuned theory text
src/HOL/Quotient.thy

2010-11-29 haftmann [Mon, 29 Nov 2010 22:41:17 +0100] rev 40817
replaced slightly odd locale congruent2 by plain definition
src/HOL/Equiv_Relations.thy src/HOL/RealDef.thy

2010-11-29 haftmann [Mon, 29 Nov 2010 22:32:06 +0100] rev 40816
replaced slightly odd locale congruent by plain definition
src/HOL/Equiv_Relations.thy src/HOL/Rat.thy src/HOL/RealDef.thy