src/HOL/Proofs/Extraction/QuotRem.thy
changeset 68048 0b4fb9fd91b1
parent 67320 6afba546f0e5