src/HOL/Tools/inductive_realizer.ML
changeset 21737 f2be09171c9c
parent 21646 c07b5b0e8492
child 21858 05f57309170c
equal deleted inserted replaced
21736:ccb2346ee416 21737:f2be09171c9c