src/HOL/Tools/inductive_set.ML
changeset 78740 45ff003d337c
parent 78095 bc42c074e58f
child 78812 d769a183d51d
equal deleted inserted replaced
78739:08fedb5bdeb0 78740:45ff003d337c