author | wenzelm |
Sun, 30 Jul 2000 13:02:14 +0200 | |
changeset 9473 | 7d13a5ace928 |
parent 5323 | 028e00595280 |
permissions | -rw-r--r-- |
4907 | 1 |
(* Title: HOL/Lex/Scanner.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TUM |
|
5 |
*) |
|
6 |
||
5069 | 7 |
Goal |
5323 | 8 |
"DA.accepts (na2da(rexp2na r)) w = (w : lang r)"; |
9 |
by (simp_tac (simpset() addsimps [NA_DA_equiv RS sym,accepts_rexp2na]) 1); |
|
10 |
qed "accepts_na2da_rexp2na"; |
|
11 |
||
12 |
Goal |
|
4907 | 13 |
"DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"; |
5132 | 14 |
by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1); |
4907 | 15 |
qed "accepts_nae2da_rexp2nae"; |