src/HOL/Library/Quotient_Sum.thy
changeset 82772 59b937edcff8
parent 67399 eab6ce8368fa
equal deleted inserted replaced
82770:4a1320dac3f3 82772:59b937edcff8