# HG changeset patch # User urbanc # Date 1315915253 0 # Node ID b1946e131ce8730162734c3d4083a4af050a5059 # Parent 061b32d78471703041a5a1074b8af8cff86871bb small typo diff -r 061b32d78471 -r b1946e131ce8 Journal/Paper.thy --- a/Journal/Paper.thy Mon Sep 12 19:50:21 2011 +0000 +++ b/Journal/Paper.thy Tue Sep 13 12:00:53 2011 +0000 @@ -2032,8 +2032,8 @@ "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same partitions. So if one is finite, the other is too, and vice versa. As noted earlier, our algorithm for solving equational systems - actually calculates the regular expression for the complement language. - Calculating this regular expression via + actually calculates a regular expression for the complement language. + Calculating such a regular expression via automata using the standard method would be quite involved. It includes the steps: regular expression @{text "\"} non-deterministic automaton @{text "\"} deterministic automaton @{text "\"} complement automaton @{text "\"}