(* Author: Tobias Nipkow *) section "Regular expressions" theory Regular_Exp imports Regular_Set begin