src/HOL/Tools/inductive_realizer.ML
changeset 19407 7c7a2e337504
parent 19046 bc5c6c9b114e
child 19473 d87a8838afa4