src/HOL/Tools/inductive_realizer.ML
changeset 29526 0b32c8b84d3e
parent 29389 0a49f940d729
child 29579 cb520b766e00
equal deleted inserted replaced
29525:ad7991d7b5bb 29526:0b32c8b84d3e