src/HOLCF/ex/Focus_ex.thy
changeset 39111 2e9bdc6fbedf
parent 37598 893dcabf0c04
child 39159 0dec18004e75