src/HOL/Tools/inductive_realizer.ML
changeset 19818 5c5c1208a3fa
parent 19806 f860b7a98445
child 20071 8f3e1ddb50e6