src/HOL/Finite_Set.ML
changeset 12397 6766aa05e4eb
parent 12396 2298d5b8e530
child 12693 827818b891c7
equal deleted inserted replaced
12396:2298d5b8e530 12397:6766aa05e4eb