src/HOL/Induct/LFilter.thy
changeset 22690 0b08f218f260
parent 21404 eb85850d3eb7
child 23746 a455e69c31cc
equal deleted inserted replaced
22689:b800228434a8 22690:0b08f218f260