src/HOL/Tools/inductive_realizer.ML
changeset 45724 1f5fc44254d7
parent 45701 615da8b8d758
child 45839 43a5b86bc102
equal deleted inserted replaced
45723:75691bcc2c0f 45724:1f5fc44254d7