src/HOL/Tools/inductive_realizer.ML
changeset 19402 742b7934ccfc
parent 19046 bc5c6c9b114e
child 19473 d87a8838afa4