src/LCF/ex/Ex4.thy
changeset 12476 eca43a50e4a4
parent 4905 be73ddff6c5a
child 17248 81bf91654e73