| changeset 5069 | 3ea049f7979d |
| parent 4907 | 0eb6730de30f |
| child 5132 | 24f992a25adc |
--- a/src/HOL/Lex/Scanner.ML Mon Jun 22 17:13:09 1998 +0200 +++ b/src/HOL/Lex/Scanner.ML Mon Jun 22 17:26:46 1998 +0200 @@ -4,7 +4,7 @@ Copyright 1998 TUM *) -goal thy +Goal "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"; by(simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1); qed "accepts_nae2da_rexp2nae";