diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,1 +1,3 @@
-0.4: Fixes definiiton of `geq`
+0.5.1:  Add 'define' commands
+0.5:    Adds more bit-wise operations
+0.4:    Fixes definiiton of `geq`
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -27,6 +27,8 @@
   , pop, popMany
   , declare
   , declareFun
+  , define
+  , defineFun
   , assert
   , check
   , Result(..)
@@ -289,6 +291,30 @@
 declareFun proc f as r =
   do ackCommand proc $ fun "declare-fun" [ Atom f, List as, r ]
      return (const f)
+
+-- | Declare a constant.  A common abbreviation for 'declareFun'.
+-- For convenience, returns the defined name as a constant expression.
+define :: Solver ->
+          String {- ^ New symbol -} ->
+          SExpr  {- ^ Symbol type -} ->
+          SExpr  {- ^ Symbol definition -} ->
+          IO SExpr
+define proc f t e = defineFun proc f [] t e
+
+-- | Define a function or a constant.
+-- For convenience, returns an the defined name as a constant expression.
+defineFun :: Solver ->
+             String           {- ^ New symbol -} ->
+             [(String,SExpr)] {- ^ Parameters, with types -} ->
+             SExpr            {- ^ Type of result -} ->
+             SExpr            {- ^ Definition -} ->
+             IO SExpr
+defineFun proc f as t e =
+  do ackCommand proc $ fun "define-fun"
+                     $ [ Atom f, List [ List [const x,a] | (x,a) <- as ], t, e]
+     return (const f)
+
+
 
 -- | Assume a fact.
 assert :: Solver -> SExpr -> IO ()
diff --git a/simple-smt.cabal b/simple-smt.cabal
--- a/simple-smt.cabal
+++ b/simple-smt.cabal
@@ -1,5 +1,5 @@
 name:                simple-smt
-version:             0.5.0
+version:             0.5.1
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3