src/HOL/Library/Indicator_Function.thy
changeset 63681 d2448471ffba
parent 63649 e690d6f2185b
child 63958 02de4a58e210