src/HOL/Library/Indicator_Function.thy
changeset 63735 fb0ae6b60491
parent 63649 e690d6f2185b
child 63958 02de4a58e210