src/HOL/ex/BinEx.thy
changeset 61306 9dd394c866fc
parent 59871 e1a49ac9c537
child 61343 5b5656a63bd6