src/HOL/Extraction/QuotRem.thy
changeset 14722 8e739a6eaf11
parent 13931 38d43d168e87
child 15244 9473137b3550