src/HOL/Tools/inductive_realizer.ML
changeset 36130 9a672f7d488d
parent 36043 d149c3886e7e
child 36610 bafd82950e24
equal deleted inserted replaced
36129:186fcdb8d00f 36130:9a672f7d488d