src/HOL/Tools/inductive_realizer.ML
changeset 58675 69571f0a93df
parent 58372 bfd497f2f4c2
child 58963 26bf09b95dda
equal deleted inserted replaced
58674:eb98d1971d2a 58675:69571f0a93df