src/HOL/ex/BinEx.thy
changeset 23017 00c0e4c42396
parent 20807 bd3b60f9a343
child 28952 15a4b2cf8c34
equal deleted inserted replaced
23016:fd7cd1edc18d 23017:00c0e4c42396