src/HOL/Extraction/QuotRem.thy
changeset 17907 c20e4bddcb11
parent 17604 5f30179fbf44
child 20593 5af400cc64d5