src/HOL/Tools/inductive_realizer.ML
changeset 70503 f0b2635ee17f
parent 70493 a9053fa30909
child 70840 5b80eb4fd0f3