src/HOL/Tools/split_rule.ML
changeset 82736 1ca8d9705e34
parent 77879 dd222e2af01a
equal deleted inserted replaced
82735:5d0d35680311 82736:1ca8d9705e34