src/HOL/Tools/inductive_realizer.ML
changeset 17076 c7effdf2e2e2
parent 16861 7446b4be013b
child 17325 d9d50222808e
equal deleted inserted replaced
17075:5e9c1b81b690 17076:c7effdf2e2e2