src/HOL/Tools/inductive_realizer.ML
changeset 13764 3e180bf68496
parent 13725 12404b452034
child 13921 69c627b6b28d
equal deleted inserted replaced
13763:f94b569cd610 13764:3e180bf68496