src/HOL/Tools/inductive_realizer.ML
changeset 18052 004515accc10
parent 18008 f193815cab2c
child 18314 4595eb4627fa