src/HOL/Tools/inductive_realizer.ML
changeset 53174 71a2702da5e0
parent 52788 da1fdbfebd39
child 54742 7a86358a3c0b
equal deleted inserted replaced
53173:b881bee69d3a 53174:71a2702da5e0