hoelzl [Tue, 26 Mar 2013 12:20:57 +0100] rev 52661
rename RealVector.thy to Real_Vector_Spaces.thy
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 52660
rename RealDef to Real
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 52659
remove Real.thy
hoelzl [Tue, 26 Mar 2013 12:20:55 +0100] rev 52658
merge RComplete into RealDef
hoelzl [Tue, 26 Mar 2013 12:20:54 +0100] rev 52657
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
hoelzl [Tue, 26 Mar 2013 12:20:53 +0100] rev 52656
remove posreal_complete
hoelzl [Tue, 26 Mar 2013 12:20:52 +0100] rev 52655
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
ballarin [Mon, 25 Mar 2013 20:00:27 +0100] rev 52654
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 52653
Remove obsolete URLs in documentation of HOL-Algebra.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 52652
Fix issue related to mixins in roundup.
Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.