# HG changeset patch
# User zhang
# Date 1296051156 0
# Node ID a3d1868ada7dc4593cc6ee16c2fd4ea33e6b76e2
# Parent  01234c4e0494d57534532794889c041da9d30175
Small modification

diff -r 01234c4e0494 -r a3d1868ada7d Myhill.thy
--- a/Myhill.thy	Wed Jan 26 13:21:16 2011 +0000
+++ b/Myhill.thy	Wed Jan 26 14:12:36 2011 +0000
@@ -2,6 +2,27 @@
   imports Main List_Prefix Prefix_subtract
 begin
 
+(*
+text {*
+     \begin{figure}
+    \centering
+    \scalebox{0.95}{
+    \begin{tikzpicture}[->,>=latex,shorten >=1pt,auto,node distance=1.2cm, semithick]
+        \node[state,initial] (n1)                   {$1$};
+        \node[state,accepting] (n2) [right = 10em of n1]   {$2$};
+
+        \path (n1) edge [bend left] node {$0$} (n2)
+            (n1) edge [loop above] node{$1$} (n1)
+            (n2) edge [loop above] node{$0$} (n2)
+            (n2) edge [bend left]  node {$1$} (n1)
+            ;
+    \end{tikzpicture}}
+    \caption{An example automaton (or partition)}\label{fig:example_automata}
+    \end{figure}
+*}
+
+*)
+
 section {* Preliminary definitions *}
 
 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}