--- a/src/HOL/Lex/Scanner.thy Mon Aug 17 11:00:27 1998 +0200 +++ b/src/HOL/Lex/Scanner.thy Mon Aug 17 11:00:57 1998 +0200 @@ -4,4 +4,4 @@ Copyright 1998 TUM *) -Scanner = Automata + RegExp2NAe +Scanner = Automata + RegExp2NA + RegExp2NAe