src/HOL/Extraction/QuotRem.thy
changeset 21404 eb85850d3eb7
parent 21125 9b7d35ca1eef
child 21545 54cc492d80a9