src/HOL/Real/ex/BinEx.thy
changeset 7577 644f9b4ae764
child 11595 6ef2535fff93
equal deleted inserted replaced
7576:594f09166c38 7577:644f9b4ae764
       
     1 
       
     2 BinEx = Real