src/HOL/Lex/RegExp2NAe.ML
changeset 7333 6cb15c6f1d9f
parent 5758 27a2b36efd95
child 7958 f531589c9fc1