src/HOL/Tools/inductive_realizer.ML
changeset 82845 d4da7d857bb7
parent 81954 6f2bcdfa9a19
equal deleted inserted replaced
82844:ebfb0e011c95 82845:d4da7d857bb7