I am trying to learn set construction in Isabelle but I am failing.
Consider you want a function that gives you all natural numbers that are smaller than a given number. I thought this should work: