src/HOL/Tools/inductive_realizer.ML
changeset 33954 1bc3b688548c
parent 33726 0878aecbf119
child 33955 fff6f11b1f09