src/HOL/Tools/inductive_realizer.ML
changeset 46118 e99ca055c91d
parent 45839 43a5b86bc102
child 46219 426ed18eba43
equal deleted inserted replaced
46117:edd50ec8d471 46118:e99ca055c91d