src/HOL/Tools/inductive_realizer.ML
changeset 37223 5226259b6fa2
parent 37136 e0c9d3e49e15
child 37236 739d8b9c59da