1
(* Title: HOL/Lex/Scanner.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1998 TUM
5
*)
6
7
Goal
8
"DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
9
by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
10
qed "accepts_nae2da_rexp2nae";