src/HOL/Real/ex/BinEx.thy
changeset 12038 343a9888e875
parent 12018 ec054019c910
child 12613 279facb4253a