src/HOL/Lex/Automata.ML
changeset 5323 028e00595280
parent 5132 24f992a25adc
child 6294 bc084e1b4d8d
--- a/src/HOL/Lex/Automata.ML	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/Automata.ML	Mon Aug 17 11:00:57 1998 +0200
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-(*** Equivalence of NA and DA --- redundant ***)
+(*** Equivalence of NA and DA ***)
 
 Goalw [na2da_def]
  "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";