src/HOL/Tools/inductive_realizer.ML
changeset 46391 8d8d3c1f1854
parent 46219 426ed18eba43
child 46708 b138dee7bed3