src/HOL/Extraction/QuotRem.thy
changeset 15789 4cb16144c81b
parent 15244 9473137b3550
child 16417 9bc16273c2d4