src/HOL/Tools/inductive_realizer.ML
changeset 28662 64ab5bb68d4c
parent 28328 9a647179c1e6
child 28800 48f7bfebd31d