src/HOL/ex/IntRingDefs.thy
changeset 5911 7da8033264fa
parent 5601 b6456ccd9e3e
equal deleted inserted replaced
5910:151ee1a5c09c 5911:7da8033264fa