src/HOL/Tools/inductive_realizer.ML
changeset 70708 3e11f35496b3
parent 70493 a9053fa30909
child 70840 5b80eb4fd0f3