src/HOL/ex/BinEx.thy
changeset 23817 ee3ee9ea0d34
parent 20807 bd3b60f9a343
child 28952 15a4b2cf8c34
equal deleted inserted replaced
23816:3879cb3d0ba7 23817:ee3ee9ea0d34