src/HOL/Tools/inductive_realizer.ML
changeset 19407 7c7a2e337504
parent 19046 bc5c6c9b114e
child 19473 d87a8838afa4
equal deleted inserted replaced
19406:410b9d9bf9a1 19407:7c7a2e337504