src/HOL/Rat.thy
changeset 58377 c6f93b8d2d8e
parent 57576 083dfad2727c
child 58410 6d46ad54a2ab