src/HOL/Rat.thy
changeset 69544 5aa5a8d6e5b5
parent 68547 549a4992222f
child 69593 3dda49e08b9d