changeset 67006 | b1278ed3cd46 |
parent 66453 | cc19f7ca2ed6 |
child 67613 | ce654b0e6d69 |
--- a/src/HOL/ex/Birthday_Paradox.thy Sat Nov 04 18:57:49 2017 +0100 +++ b/src/HOL/ex/Birthday_Paradox.thy Sat Nov 04 19:17:19 2017 +0100 @@ -5,7 +5,7 @@ section \<open>A Formulation of the Birthday Paradox\<close> theory Birthday_Paradox -imports Main HOL.Binomial "HOL-Library.FuncSet" +imports Main "HOL-Library.FuncSet" begin section \<open>Cardinality\<close>