src/HOL/IMP/Collecting.thy
changeset 82845 d4da7d857bb7
parent 80914 d97fdabd9e2b
equal deleted inserted replaced
82844:ebfb0e011c95 82845:d4da7d857bb7