# HG changeset patch
# User nipkow
# Date 905857763 -7200
# Node ID 15c97b95b3e304888af8a9105f001be86c192108
# Parent  9df083aed63d1527f9b53d58d5c22f656978b0f3
Function 'step' is already defined in NA.thy.

diff -r 9df083aed63d -r 15c97b95b3e3 src/HOL/Lex/NAe.thy
--- a/src/HOL/Lex/NAe.thy	Tue Sep 15 10:40:40 1998 +0200
+++ b/src/HOL/Lex/NAe.thy	Tue Sep 15 13:09:23 1998 +0200
@@ -10,10 +10,6 @@
 
 types ('a,'s)nae = ('a option,'s)na
 
-constdefs
- step :: "('a,'s)nae => 'a option => ('s * 's)set"
-"step A a == {(p,q) . q : next A a p}"
-
 syntax eps :: "('a,'s)nae => ('s * 's)set"
 translations "eps A" == "step A None"