diff --git a/README.md b/README.md
index e8b2202..d7593bd 100644
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@ cargo add smtlib
 Now you can go ahead and use the library in your project.
 
 ```rust
-use smtlib::{backend::z3_binary::Z3Binary, Int, SatResultWithModel, Solver, Sort};
+use smtlib::{backend::z3_binary::Z3Binary, Int, SatResultWithModel, Solver, prelude::*};
 
 fn main() -> Result<(), Box<dyn std::error::Error>> {
     // Initialize the solver with the Z3 backend. The "z3" string refers the
@@ -38,8 +38,8 @@ fn main() -> Result<(), Box<dyn std::error::Error>> {
     let mut solver = Solver::new(Z3Binary::new("z3")?)?;
 
     // Declare two new variables
-    let x = Int::from_name("x");
-    let y = Int::from_name("y");
+    let x = Int::new_const("x");
+    let y = Int::new_const("y");
 
     // Assert some constraints. This tells the solver that these expressions
     // must be true, so any solution will satisfy these.
diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs
index f89ce56..50a08c5 100644
--- a/smtlib/src/lib.rs
+++ b/smtlib/src/lib.rs
@@ -167,10 +167,10 @@ impl Model {
     /// expression asserted.
     ///
     /// ```
-    /// # use smtlib::{Int, Sort};
+    /// # use smtlib::{Int, prelude::*};
     /// # fn main() -> Result<(), Box<dyn std::error::Error>> {
     /// # let mut solver = smtlib::Solver::new(smtlib::backend::z3_binary::Z3Binary::new("z3")?)?;
-    /// let x = Int::from_name("x");
+    /// let x = Int::new_const("x");
     /// solver.assert(x._eq(12))?;
     /// let model = solver.check_sat_with_model()?.expect_sat()?;
     /// match model.eval(x) {
diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs
index 48a433c..10a2510 100644
--- a/smtlib/src/solver.rs
+++ b/smtlib/src/solver.rs
@@ -15,14 +15,14 @@ use crate::{
 /// The [`Solver`] type is the primary entrypoint to interaction with the
 /// solver. Checking for validity of a set of assertions requires:
 /// ```
-/// # use smtlib::{Int, Sort};
+/// # use smtlib::{Int, prelude::*};
 /// # fn main() -> Result<(), Box<dyn std::error::Error>> {
 /// // 1. Set up the backend (in this case z3)
 /// let backend = smtlib::backend::z3_binary::Z3Binary::new("z3")?;
 /// // 2. Set up the solver
 /// let mut solver = smtlib::Solver::new(backend)?;
 /// // 3. Declare the necessary constants
-/// let x = Int::from_name("x");
+/// let x = Int::new_const("x");
 /// // 4. Add assertions to the solver
 /// solver.assert(x._eq(12))?;
 /// // 5. Check for validity, and optionally construct a model
diff --git a/smtlib/src/tokio_solver.rs b/smtlib/src/tokio_solver.rs
index f624fa9..c828277 100644
--- a/smtlib/src/tokio_solver.rs
+++ b/smtlib/src/tokio_solver.rs
@@ -12,7 +12,7 @@ use crate::{Bool, Error, Logic, Model, SatResult, SatResultWithModel};
 /// The [`TokioSolver`] type is the primary entrypoint to interaction with the
 /// solver. Checking for validity of a set of assertions requires:
 /// ```
-/// # use smtlib::{Int, Sort};
+/// # use smtlib::{Int, prelude::*};
 /// # fn main() -> Result<(), Box<dyn std::error::Error>> {
 /// # tokio_test::block_on(async {
 /// // 1. Set up the backend (in this case z3)
@@ -20,7 +20,7 @@ use crate::{Bool, Error, Logic, Model, SatResult, SatResultWithModel};
 /// // 2. Set up the solver
 /// let mut solver = smtlib::TokioSolver::new(backend).await?;
 /// // 3. Declare the necessary constants
-/// let x = Int::from_name("x");
+/// let x = Int::new_const("x");
 /// // 4. Add assertions to the solver
 /// solver.assert(x._eq(12)).await?;
 /// // 5. Check for validity, and optionally construct a model