src/HOLCF/Discrete0.thy
changeset 14610 9c2e31e483b2
parent 12338 de0f4a63baa5
child 14981 e73f8140af78