src/HOL/Tools/inductive_realizer.ML
changeset 24819 7d8e0a47392e
parent 24816 2d0fa8f31804
child 24926 bcb6b098df11