Tue, 26 Mar 2013 12:20:56 +0100 remove Real.thy
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 51522
remove Real.thy
Tue, 26 Mar 2013 12:20:55 +0100 merge RComplete into RealDef
hoelzl [Tue, 26 Mar 2013 12:20:55 +0100] rev 51521
merge RComplete into RealDef
Tue, 26 Mar 2013 12:20:54 +0100 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:54 +0100] rev 51520
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
Tue, 26 Mar 2013 12:20:53 +0100 remove posreal_complete
hoelzl [Tue, 26 Mar 2013 12:20:53 +0100] rev 51519
remove posreal_complete
Tue, 26 Mar 2013 12:20:52 +0100 separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl [Tue, 26 Mar 2013 12:20:52 +0100] rev 51518
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
Mon, 25 Mar 2013 20:00:27 +0100 Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin [Mon, 25 Mar 2013 20:00:27 +0100] rev 51517
Discontinued theories src/HOL/Algebra/abstract and .../poly.
Mon, 25 Mar 2013 19:53:44 +0100 Remove obsolete URLs in documentation of HOL-Algebra.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51516
Remove obsolete URLs in documentation of HOL-Algebra.
Mon, 25 Mar 2013 19:53:44 +0100 Fix issue related to mixins in roundup.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51515
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.
Mon, 25 Mar 2013 15:18:44 +0100 simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing [Mon, 25 Mar 2013 15:18:44 +0100] rev 51514
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
Mon, 25 Mar 2013 15:09:41 +0100 added lemmas
nipkow [Mon, 25 Mar 2013 15:09:41 +0100] rev 51513
added lemmas
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip