src/HOL/ex/BT.thy
changeset 22330 00ca68f5ce29
parent 20711 8b52cdaee86c
child 23023 7b52c4fde622