diff --git a/language-gcl.cabal b/language-gcl.cabal
--- a/language-gcl.cabal
+++ b/language-gcl.cabal
@@ -1,5 +1,5 @@
 name:               language-gcl
-version:            0.1
+version:            0.2
 synopsis:           Something similar to Dijkstra's guarded command language
 description:
     language-gcl provides the abstract syntax and parsers for
@@ -13,6 +13,7 @@
 build-type:         Simple
 cabal-version:      >=1.10
 tested-with:        GHC==7.6.3
+extra-source-files: samples/ParseSample.hs, samples/*.txt
 
 library
     exposed-modules:
diff --git a/samples/ParseSample.hs b/samples/ParseSample.hs
new file mode 100644
--- /dev/null
+++ b/samples/ParseSample.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE Haskell2010 #-}
+module Main where
+
+import Control.Applicative
+import Text.Parser.Char
+import Text.Parser.Combinators
+import Text.Parser.Token
+import qualified Data.Attoparsec.Text as AT
+import qualified Data.Text as T
+import System.IO
+
+import Language.GuardedCommands
+
+main :: IO ()
+main = do
+    c <- T.pack <$> getContents
+    case AT.parseOnly (optional someSpace *> pGCL pVoid (pBoolExpr pVar) <* AT.endOfInput) c of
+        Left e -> hPutStrLn stderr e
+        Right v -> print v
+
+data BoolExpr a
+    = And (BoolExpr a) (BoolExpr a)
+    | Or  (BoolExpr a) (BoolExpr a)
+    | Literal Bool
+    | Atom a
+    deriving Show
+
+pBoolExpr :: TokenParsing m => m atom -> m (BoolExpr atom)
+pBoolExpr pAtom = p0
+  where
+    p0 = flOr  <$> p1 <*> many (symbol "\\/" *> p1)
+    p1 = flAnd <$> p2 <*> many (symbol "/\\" *> p2)
+    p2 = between (symbol "(") (symbol ")") p0
+        <|> Literal True <$ symbol "true"
+        <|> Literal False <$ symbol "false"
+        <|> Atom <$> pAtom
+
+    flOr  x xs = foldr1 Or  (x:xs)
+    flAnd x xs = foldr1 And (x:xs)
+
+pVar :: TokenParsing m => m String
+pVar = token (some upper)
+
+data Void
+
+instance Show Void where
+    show _ = ""
+
+pVoid :: Alternative m => m Void
+pVoid = empty
diff --git a/samples/sample1.txt b/samples/sample1.txt
new file mode 100644
--- /dev/null
+++ b/samples/sample1.txt
@@ -0,0 +1,5 @@
+invariant P
+invariant Q \/ P /\ R
+invariant R
+do X /\ Y → skip; abort
+ ⫾ true   → while Z do skip od od
diff --git a/src/Language/GuardedCommands.hs b/src/Language/GuardedCommands.hs
--- a/src/Language/GuardedCommands.hs
+++ b/src/Language/GuardedCommands.hs
@@ -39,7 +39,7 @@
       -- | Parsers based on the 'Text.Parser.Combinators.TokenParsing' class.
       --
       --   By overriding 'Text.Parser.Combinators.TokenParsing.token' appropriately,
-      --   the keywords (@words \"□ → if fi do od abort skip invariant while  \"@)
+      --   the keywords (@words \"⫾ → if fi do od abort skip invariant while  \"@)
       --   may take on different forms or even be forbidden.
     , pGCL
     , pGuardedCommandSet
@@ -57,10 +57,10 @@
 
 -- | Guarded statements
 data GCL stmt guard
-    = -- | Alternative statement.
+      -- | Alternative statement.
       -- If none of the guards is true, the command diverges;
       -- otherwise, an arbitrary guarded list with a true guard is executed.
-       Alternative           [GC stmt guard]
+    =  Alternative           [GC stmt guard]
       -- | Repetitive statement.
       -- If none of the guards is true, the command terminates;
       -- otherwise, an arbitrary guarded list with a true guard is executed (the \'iteration\'),
@@ -69,7 +69,7 @@
     |  Repetitive   [guard]  [GC stmt guard]
       -- | Some user-defined statement.
     |  Statement   stmt
-    deriving (Eq,Foldable,Functor,Data,Traversable,Typeable)
+    deriving (Data,Eq,Foldable,Functor,Show,Traversable,Typeable)
 
 instance Bifunctor GCL where
     bimap f g (Alternative gss) = Alternative (map (bimap f g) gss)
@@ -78,7 +78,7 @@
 
 -- | Guarded commands
 data GC stmt guard = GC guard [GCL stmt guard]
-    deriving (Eq,Foldable,Functor,Data,Traversable,Typeable)
+    deriving (Data,Eq,Foldable,Functor,Show,Traversable,Typeable)
 
 instance Bifunctor GC where
     bimap f g (GC gd gl) = GC (g gd) (map (bimap f g) gl)
@@ -99,7 +99,7 @@
 
     pSelf = Alternative <$> pGcsBlock "if" "fi"
         <|> procWhile <$> symbol "while" <*> pGuard <*> pLoopInvs
-        <*> between (symbol "do") (symbol "od") (pGuardedList pSelf)
+        <*> between (symbol "do") (symbol "od") (option [] $ pGuardedList pSelf)
         <|> Repetitive <$> pLoopInvs <*> pGcsBlock "do" "od"
         <|> Alternative [] <$ symbol "abort"
         <|> Repetitive [] [] <$ symbol "skip"
@@ -109,14 +109,13 @@
 
 -- | Parse a guarded command set, given parsers for guards and guarded statements.
 --
---   The guarded commands are separated by a 'white box' (U+25A1) symbol,
---   although one might argue that Dijkstra used a 'white vertical rectangle' (U+25AF).
+--   The guarded commands are separated by a 'white vertical bar' (U+2AFE) symbol,
+--   a.k.a. 'Dijkstra choice'.
 pGuardedCommandSet
     :: TokenParsing m
     => m guard -> m (GCL stmt guard) -> m [GC stmt guard]
 pGuardedCommandSet pGuard pTheGCL
-    = pGuardedCommand pGuard pTheGCL `sepBy` symbol "□"
-    -- There are a few alternatives (U+25AF, U+25 or the string @"[]"@)
+    = pGuardedCommand pGuard pTheGCL `sepBy` symbol "⫾"
 
 -- | Parse a guarded command, given parsers for guards and guarded statements.
 --