src/HOL/Tools/inductive_realizer.ML
changeset 29263 bf99ccf71b7c
parent 28965 1de908189869
child 29265 5b4247055bd7