src/HOL/Tools/inductive_realizer.ML
changeset 82910 aa3b2d384736
parent 81954 6f2bcdfa9a19
equal deleted inserted replaced
82909:e4fae2227594 82910:aa3b2d384736