src/HOL/Tools/split_rule.ML
changeset 82845 d4da7d857bb7
parent 77879 dd222e2af01a
equal deleted inserted replaced
82844:ebfb0e011c95 82845:d4da7d857bb7