wenzelm [Tue, 26 Mar 2013 19:43:31 +0100] rev 51541
tuned proofs;
haftmann [Tue, 26 Mar 2013 20:49:57 +0100] rev 51540
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
wenzelm [Tue, 26 Mar 2013 15:10:28 +0100] rev 51539
merged
wenzelm [Tue, 26 Mar 2013 14:38:44 +0100] rev 51538
proper input event handling;
wenzelm [Tue, 26 Mar 2013 14:14:39 +0100] rev 51537
more standard imports;
wenzelm [Tue, 26 Mar 2013 14:05:08 +0100] rev 51536
more specific Entry painting;
ignore theories with all commands below threshold;
wenzelm [Tue, 26 Mar 2013 14:03:31 +0100] rev 51535
tuned;
wenzelm [Tue, 26 Mar 2013 12:40:51 +0100] rev 51534
mixed theory/command entries;
tuned;
wenzelm [Tue, 26 Mar 2013 11:26:13 +0100] rev 51533
dockable window for timing information;
kleing [Tue, 26 Mar 2013 13:54:24 +0100] rev 51532
no \FIXME macro for ProgProve (moved to book)
hoelzl [Tue, 26 Mar 2013 12:21:01 +0100] rev 51531
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl [Tue, 26 Mar 2013 12:21:00 +0100] rev 51530
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
hoelzl [Tue, 26 Mar 2013 12:21:00 +0100] rev 51529
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
hoelzl [Tue, 26 Mar 2013 12:20:59 +0100] rev 51528
Series.thy is based on Limits.thy and not Deriv.thy
hoelzl [Tue, 26 Mar 2013 12:20:59 +0100] rev 51527
move Ln.thy and Log.thy to Transcendental.thy
hoelzl [Tue, 26 Mar 2013 12:20:58 +0100] rev 51526
move SEQ.thy and Lim.thy to Limits.thy
hoelzl [Tue, 26 Mar 2013 12:20:58 +0100] rev 51525
HOL-NSA should only import Complex_Main
hoelzl [Tue, 26 Mar 2013 12:20:57 +0100] rev 51524
rename RealVector.thy to Real_Vector_Spaces.thy
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 51523
rename RealDef to Real
hoelzl [Tue, 26 Mar 2013 12:20:56 +0100] rev 51522
remove Real.thy
hoelzl [Tue, 26 Mar 2013 12:20:55 +0100] rev 51521
merge RComplete into RealDef
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
hoelzl [Tue, 26 Mar 2013 12:20:53 +0100] rev 51519
remove posreal_complete
hoelzl [Tue, 26 Mar 2013 12:20:52 +0100] rev 51518
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
ballarin [Mon, 25 Mar 2013 20:00:27 +0100] rev 51517
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51516
Remove obsolete URLs in documentation of HOL-Algebra.
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.
kleing [Mon, 25 Mar 2013 15:18:44 +0100] rev 51514
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold