src/Pure/ROOT.ML
changeset 81473 53e61087bc6f
parent 81456 b29b72f64a6c
child 81581 8a3608933607
equal deleted inserted replaced
81472:e43bff789ac0 81473:53e61087bc6f