src/HOL/ex/Sum_of_Powers.thy
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-10-06 wenzelm 2015-10-06 isabelle update_cartouches;
2015-06-12 bulwahn 2015-06-12 add examples from Freek's top 100 theorems (thms 30, 73, 77)