# HG changeset patch
# User nipkow
# Date 1011292677 -3600
# Node ID c992ee4168ff30042cda01db4dd10f6a4ee51f08
# Parent  e99d4a6cba8b579bd2dc65ca14129046aec9fb6e
new style theory

diff -r e99d4a6cba8b -r c992ee4168ff src/HOL/Lex/Scanner.ML
--- a/src/HOL/Lex/Scanner.ML	Thu Jan 17 19:37:42 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/Lex/Scanner.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998 TUM
-*)
-
-Goal
- "DA.accepts (na2da(rexp2na r)) w = (w : lang r)";
-by (simp_tac (simpset() addsimps [NA_DA_equiv RS sym,accepts_rexp2na]) 1);
-qed "accepts_na2da_rexp2na";
-
-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";