src/HOL/Library/Indicator_Function.thy
changeset 63761 2ca536d0163e
parent 63649 e690d6f2185b
child 63958 02de4a58e210
equal deleted inserted replaced
63760:b1088b1e3b7e 63761:2ca536d0163e