diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -12,7 +12,7 @@
 
 @
 float a = 0.0;            a <- 'float' \"a\" 0
-bool b = true;            b <- 'bool' \"b\" true
+bool b = true;            b <- 'bool' \"b\" True
 int c = d + e + 3;        c <- 'int'' \"c\" (d + e + 3)
 @
 
@@ -52,7 +52,7 @@
 /Statement Labels/
 
 @
-hello: {                  \"hello\" '-:' do
+label: {                  \"label\" '|-' do
     a();                      a
     b();                      b
 }
@@ -94,8 +94,8 @@
 a + b                     a '+' b
 a * b                     a '*.' b
 a \/ b                     a '/.' b     -- float
-a \/ b                     a '`div_`' b -- int
-a % b                     a '`mod_`' b
+a \/ b                     'div_' a b   -- int
+a % b                     'mod_' a b
 abs(a)                    'abs' a
 min(a, b)                 'min_' a b
 max(a, b)                 'max_' a b
@@ -106,7 +106,7 @@
 @
 
 /Function Definitions and Function Calls/
-(All ImProve functions are Haskell functions that are inlined at compile time.)
+(All ImProve functions are Haskell functions, which are inlined at code generation.)
 
 @
 int add(int a, int b) {                             add :: E Int -> E Int -> E Int
@@ -123,6 +123,12 @@
 @
 
 -}
+
+-- hello: \{                  hello '+++' do
+--     a();                      a
+--     b();                      b
+--
+
 module Language.ImProve
   (
   -- * Types
@@ -172,8 +178,8 @@
   -- * Statements
   , Stmt
   -- ** Statement Labeling and Hierarchical Scope
-  , (-:)
-  , (!)
+  , (|=)
+  , (|-)
   -- ** Variable Declarations
   , bool
   , bool'
@@ -210,7 +216,7 @@
 infixl 3 &&.
 infixl 2 ||.
 infixr 1 -->
-infixr 0 <==, -:, !
+infixr 0 <==, |-, |=
 
 -- | True term.
 true :: E Bool
@@ -252,7 +258,7 @@
 any_ :: (a -> E Bool) -> [a] -> E Bool
 any_ f a = or_ $ map f a
 
--- Logical implication (if a then b).
+-- | Logical implication.
 (-->) :: E Bool -> E Bool -> E Bool 
 a --> b = not_ a ||. b
 
@@ -342,8 +348,8 @@
 -- | Labels a statement.
 --   Labels are used in counter examples to trace the program execution.
 --   And assertion names, and hence counter example trace file names, are produce from labels.
-(-:) :: Name -> Stmt a -> Stmt a
-name -: stmt = do
+(|-) :: Name -> Stmt a -> Stmt a
+name |- stmt = do
   (path0, stmt0) <- get
   put (path0, Null)
   a <- stmt
@@ -353,8 +359,8 @@
   return a
 
 -- | Creates a new hierarcical scope for variable names.
-(!) :: Name -> Stmt a -> Stmt a
-name ! stmt = do
+(|=) :: Name -> Stmt a -> Stmt a
+name |= stmt = do
   (path0, stmt0) <- get
   put (path0 ++ [name], stmt0)
   a <- stmt
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -25,18 +25,18 @@
   b1 <- int "b1" 0  -- Working copy of 'b'.
 
   -- A new input to process.
-  "startNew" -: if_ (a /=. ref a0 ||. b /=. ref b0) $ do
+  "startNew" |- if_ (a /=. ref a0 ||. b /=. ref b0) $ do
     a0 <== a
     b0 <== b
     a1 <== a
     b1 <== b
 
   -- Reduce a1.
-  "reduceA" -: if_ (ref a1 >. ref b1) $ do
+  "reduceA" |- if_ (ref a1 >. ref b1) $ do
     a1 <== ref a1 - ref b1
 
   -- Reduce b1.
-  "reduceB" -: if_ (ref b1 >. ref a1) $ do
+  "reduceB" |- if_ (ref b1 >. ref a1) $ do
     b1 <== ref b1 - ref a1
 
   -- Done if a1 == b1.
@@ -52,7 +52,7 @@
   result <- int  "result" 0      -- Result of GCD.
 
   -- Call gcd' in its own scope.  (Scopes prevent variable name collisions.)
-  (done', result') <- "gcd" ! gcd' a b
+  (done', result') <- "gcd" |= gcd' a b
 
   -- Bind the results to the output variables.
   done   <== done'
@@ -72,8 +72,8 @@
   counter <- int "counter" 0
 
   -- Specification.
-  "GreaterThanOrEqualTo0" -: assert $ ref counter >=. 0
-  "LessThan10"            -: assert $ ref counter <.  10
+  "GreaterThanOrEqualTo0" |- assert $ ref counter >=. 0
+  "LessThan10"            |- assert $ ref counter <.  10
 
   -- Implementation.
   ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)
@@ -93,25 +93,25 @@
 arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
 
   -- Mutual exclusion.  At most, only one requester granted at a time.
-  "OneHot" -: assert $      grantA &&. not_ grantB &&. not_ grantC
+  "OneHot" |- assert $      grantA &&. not_ grantB &&. not_ grantC
                    ||. not_ grantA &&.      grantB &&. not_ grantC
                    ||. not_ grantA &&. not_ grantB &&.      grantC
                    ||. not_ grantA &&. not_ grantB &&. not_ grantC
   
   -- No grants without requests.
-  "NotRequestedA" -: assert $ not_ requestA --> not_ grantA
-  "NotRequestedB" -: assert $ not_ requestB --> not_ grantB
-  "NotRequestedC" -: assert $ not_ requestC --> not_ grantC
+  "NotRequestedA" |- assert $ not_ requestA --> not_ grantA
+  "NotRequestedB" |- assert $ not_ requestB --> not_ grantB
+  "NotRequestedC" |- assert $ not_ requestC --> not_ grantC
 
   -- Grants to single requests.
-  "OnlyRequestA" -: assert $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA
-  "OnlyRequestB" -: assert $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB
-  "OnlyRequestC" -: assert $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC
+  "OnlyRequestA" |- assert $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA
+  "OnlyRequestB" |- assert $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB
+  "OnlyRequestC" |- assert $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC
 
   -- Priority.
-  "Highest" -: assert $ requestA --> grantA
-  "Medium"  -: assert $ (not_ requestA &&. requestB) --> grantB
-  "Lowest"  -: assert $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
+  "Highest" |- assert $ requestA --> grantA
+  "Medium"  |- assert $ (not_ requestA &&. requestB) --> grantB
+  "Lowest"  |- assert $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
 
 -- | An arbiter implementation.
 arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
@@ -128,9 +128,9 @@
   grantB <- bool "grantB" False
   grantC <- bool "grantC" False
 
-  "GrantA" -: if_ (requestA)                                     (grantA <== true)
-  "GrantB" -: if_ (not_ requestA &&. requestB)                   (grantB <== true)
-  "GrantC" -: if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
+  "GrantA" |- if_ (requestA)                                     (grantA <== true)
+  "GrantB" |- if_ (not_ requestA &&. requestB)                   (grantB <== true)
+  "GrantC" |- if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
 
   return (ref grantA, ref grantB, ref grantC)
 
@@ -144,7 +144,7 @@
 
 -- | Binding an arbiter implemenation to the arbiter specification.
 arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()
-arbiter name implementation = name -: do
+arbiter name implementation = name |- do
   -- Create input variables.
   requestA <- input bool "requestA"
   requestB <- input bool "requestB"
@@ -152,7 +152,7 @@
   let requests = (requestA, requestB, requestC)
 
   -- Instantiate implementation.
-  grants@(grantA, grantB, grantC) <- "impl" -: implementation requests
+  grants@(grantA, grantB, grantC) <- "impl" |- implementation requests
 
   -- Bind specification.
   arbiterSpec requests grants
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.0.9
+version: 0.0.10
 
 category: Language