src/HOL/Tools/inductive_realizer.ML
changeset 28724 4656aacba2bc
parent 28328 9a647179c1e6
child 28800 48f7bfebd31d