src/HOL/ex/Ballot.thy
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
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-16 hoelzl 2015-06-16 tuned src/HOL/ex/Ballot
2015-06-12 bulwahn 2015-06-12 add examples from Freek's top 100 theorems (thms 30, 73, 77)