src/HOL/Tools/inductive_realizer.ML
changeset 58488 289d1c39968c
parent 58372 bfd497f2f4c2
child 58963 26bf09b95dda
equal deleted inserted replaced
58487:1ae4ab94ea63 58488:289d1c39968c