src/HOL/Library/Indicator_Function.thy
changeset 62005 68db98c2cd97
parent 61969 e01015e49041
child 62390 842917225d56
equal deleted inserted replaced
62004:8c6226d88ced 62005:68db98c2cd97