src/HOL/Library/Indicator_Function.thy
changeset 61686 e6784939d645
parent 61633 64e6d712af16
child 61954 1d43f86f48be