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)";