diff --git a/docs/user-guide/src/SUMMARY.md b/docs/user-guide/src/SUMMARY.md
index 10edf7c0b80..a8f6239eab8 100644
--- a/docs/user-guide/src/SUMMARY.md
+++ b/docs/user-guide/src/SUMMARY.md
@@ -17,6 +17,7 @@
   - [Final Code](tour/final.md)
   - [Loop Invariants](tour/loop_invariants.md)
   - [Counterexamples](tour/counterexamples.md)
+  - [`prusti-std` and External Specifications](tour/extern_specs.md)
 - [Verification Features](verify/summary.md)
   - [Absence of panics](verify/panic.md)
   - [Overflow checks](verify/overflow.md)
diff --git a/docs/user-guide/src/tour/extern_specs.md b/docs/user-guide/src/tour/extern_specs.md
new file mode 100644
index 00000000000..1c0dfa80ef7
--- /dev/null
+++ b/docs/user-guide/src/tour/extern_specs.md
@@ -0,0 +1,42 @@
+# `prusti-std` and External Specifications
+
+In the previous chapters, the code we verified included calls to functions provided by the standard library, such as `std::mem::replace`. Prusti verifies code in a *function modular* fashion, so it only considers the specification of a function in order to verify a call to it. By default, external functions are assumed to have the contract `#[requires(true)]`, `#[ensures(true)]`, i.e. it is always possible to call the function, but it does not guarantee anything.
+
+`prusti-std` is a crate that is part of the Prusti project. It provides specifications for some standard library methods. It does not provide specifications for *all* standard library methods, but the aim is to provide a high coverage of calls, based on data found in real Rust code, evaluated on the top crates of `crates.io`.
+
+The documentation of `prusti-std` provides an overview of the specified methods, as well as informal descriptions of the contracts.
+
+## Creating new external specifications
+
+When the specification for an external method is not provided (for example, because it is not in `prusti-std`), it is likely that verification of code using that method will fail. To provide the contract for an external method, an [*external specification*](../verify/external.md) should be declared.
+
+For the sake of example, assume the `std::mem::replace` method was *not* specified in `prusti-std`. We could provide an external specification for it like so:
+
+```rust,ignore
+#[extern_spec(std::mem)]
+#[ensures(snap(dest) === src)]
+#[ensures(result === old(snap(dest)))]
+fn replace<T>(dest: &mut T, src: T) -> T;
+```
+
+Let's break this snippet down step by step:
+- First, we write the Prusti annotation `#[extern_spec]` to denote that we are writing an external specification. This requires `prusti_contracts::*` to be imported first.
+- Next, we need to declare where the original function is located. In this case it is the module `std::mem`, so we put its path in the parameter: `#[extern_spec(std::mem)]`
+- After a quick search for *\"rust std mem replace\"* we can find the [documentation for std::mem::replace](https://doc.rust-lang.org/std/mem/fn.replace.html). Here we can get the function signature: `pub fn replace<T>(dest: &mut T, src: T) -> T`. We then write down the signature in the inner module, followed by a `;`. The visibility modifier is omitted for external specifications.
+- Since there are no preconditions to `replace`, we can use the (implicit) default `#[requires(true)]`.
+- For writing the postcondition, we use four pieces of Prusti syntax:
+  - [`===`](../syntax.md#snapshot-equality) is called **snapshot equality** or **logical equality**. Is means that the left and right operands are structurally equal. `===` does not require the type of the compared elements to implement [PartialEq](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html), which would be required if we used the standard equality operator `==`.
+  - The [`snap()`](../syntax.md#snap-function) function takes a snapshot of a reference. It has a similar functionality to the [`clone()`](https://doc.rust-lang.org/std/clone/trait.Clone.html) method, but does not require the type of the reference it is called on to implement the `Clone` trait. `snap` should only be used in specifications, since it ignores the borrow checker.
+  - Lastly, we have the [`old()` function](../syntax.md#old-expressions), which denotes that we want to refer to the state of `snap(dest)` from before the function was called.
+  - The identifier [`result`](../syntax.md#result-variable) is used to refer to the return parameter of the function.
+- The postcondition consists of two parts, which can either be written in one condition with `&&`, or in multiple `#[ensures(...)]` annotations like in the example above.
+  - The first condition `snap(dest) === src` means: *After the function returns, the location referenced by `dest` is structurally equal to the parameter `src`.*
+  - The second part of the postcondition is `result === old(snap(dest))`. This means: *The `result` returned by the function is structurally equal to the the element that was referenced by `dest` **before** the function was called.*
+
+Since `result` is structurally equal to `dest` from before the function call, Prusti knows that the pure function `len()` called on `result` returns the same value as it would have for `dest`.
+
+An important thing to note here is that Prusti does ***not*** check if `replace` actually does what the external specification says it does. `#[extern_spec]` implicitly implies the `#[trusted]` annotation, which means that any postconditions are just accepted and used by Prusti.
+
+### Future
+
+There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate the `extern_spec` declaration for a given call.
diff --git a/docs/user-guide/src/tour/option.md b/docs/user-guide/src/tour/option.md
index 77281396469..b22e46eca18 100644
--- a/docs/user-guide/src/tour/option.md
+++ b/docs/user-guide/src/tour/option.md
@@ -10,12 +10,6 @@ Just like in the "Learning Rust With Entirely Too Many Linked Lists" tutorial, w
 type Link = Option<Box<Node>>;
 ```
 
-In order to use the `Option::take` function, we also have to implement the `extern_spec` for it. As you can see, it is quite similar to the `extern_spec` for `mem::replace`, since `take` does the same as `replace(&mut self, None)`:
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:option_take_extern_spec}}
-```
-
 Changing the `Link` type requires some adjustments of the code and specifications. With the new type alias for `Link`, we cannot have an `impl Link` block anymore, so our `lookup` and `len` functions on `Link` are now normal, free-standing functions:
 
 ```rust,noplaypen
@@ -31,6 +25,9 @@ Due to current limitations of Prusti, we cannot replace our `link_len` and `link
 ```
 
 Since Prusti doesn't fully support closures yet, we also cannot do the rewrite to use the `Option::map` function:
+
+<!-- TODO: link capabilities/limitations chapter (closures) -->
+
 ```rust,noplaypen
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:try_pop_rewrite}}
 ```
@@ -41,4 +38,4 @@ If you want to see the full code after all the changes, expand the following cod
 ```rust,noplaypen
 // Expand to see full code up to this chapter
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:nothing}}
-```
\ No newline at end of file
+```
diff --git a/docs/user-guide/src/tour/pop.md b/docs/user-guide/src/tour/pop.md
index e5c494684c6..58182a1288d 100644
--- a/docs/user-guide/src/tour/pop.md
+++ b/docs/user-guide/src/tour/pop.md
@@ -45,18 +45,6 @@ Since we will need to check if a list is empty, we can implement a `#[pure]` fun
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/pop.rs:is_empty}}
 ```
 
-### Writing the external specifications for `Option`
-
-Since we use `Option::unwrap`, we will need an external specification for it. While we're at it, let's also write the `#[extern_spec]` for `Option::is_some` and `Option::is_none`:
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/pop.rs:extern_spec}}
-```
-
-The syntax for writing external specifications for functions associated with `Option` is slightly different to that of `std::mem::replace`, which was a standalone function.
-
-Note: In the future, you should just be able to import these external specifications using the [`prusti-std` crate](https://crates.io/crates/prusti-std). It should be available after [this PR](https://github.com/viperproject/prusti-dev/pull/1249) is merged. Until then, you can find the work in progress specifications in the PR (e.g., for [`Option::unwrap`](https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49)).
-
 ## Implementing the specification
 
 ### Writing the precondition
diff --git a/docs/user-guide/src/tour/push.md b/docs/user-guide/src/tour/push.md
index 250a5cb7c25..20114500e4d 100644
--- a/docs/user-guide/src/tour/push.md
+++ b/docs/user-guide/src/tour/push.md
@@ -44,79 +44,20 @@ pure method `len` introduced in the [previous chapter](new.md):
 
 ```rust,noplaypen
 {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:property_1}}
+// Prusti: Verifies
 ```
 
-Even though the above implementation of `push` is correct, attempting to verify it with Prusti still yields a verification error:
-
-```plain
-[Prusti: verification error] postcondition might not hold.
-```
-
-This error may look surprising at first: 
-We create a new list node that stores the the original list in its next field.
-Why is Prusti unable to realize that the length of the resulting list
-is one plus the length of the original list?
-
-The explanation is that Prusti performs *function modular* verification, 
-that is, it only uses a function's specification (instead of also consulting the 
-function's implementation) whenever it encounters a function call.
-The only exception are *pure* functions, such as `len`, where Prusti also takes the
-function body into account.
-
-
-
-### Adding external specifications to library code
-
-In our case, the function `std::mem::replace` is neither marked as `pure` nor does it
-come with a specification. Hence, Prusti assumes that it is memory safe and nothing else.
-That is, Prusti uses `true` as both pre- and postcondition of `replace`,
-which is too weak to prove the specification of `push`. According to its specification,
-`replace` could arbitrarily change the original list and thus also its length.
-Hence, we cannot conclude that the length the list returned by
-`replace(&mut self.head, Link::Empty)` coincides with the length of the original 
-list.
-
-We can remedy this issue by strengthening the specification of `replace`.
-In this tutorial, we will assume that the standard library is correct, that is, we 
-do not attempt to verify specifications for functions in external crates, 
-like `replace`. To this end, we have to add the specification to the function.
-This can be done with another piece of Prusti syntax, the [extern_spec](../verify/external.md):
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:extern_spec}}
-```
-
-Let's break this snippet down step by step:
-- First, we write the Prusti annotation `#[extern_spec]` to denote that we are writing an external specification. This requires `prusti_contracts::*` to be imported first.
-- Next, we need to declare where the original function is located. In this case it is the module `std::mem`, so we put its path in  the parameter: `#[extern_spec(std::mem)]`
-- After a quick search for *\"rust std mem replace\"* we can find the [documentation for std::mem::replace](https://doc.rust-lang.org/std/mem/fn.replace.html). Here we can get the function signature: `pub fn replace<T>(dest: &mut T, src: T) -> T`. We then write down the signature in the inner module, followed by a `;`.
-- Since there are no preconditions to `replace`, we can use the (implicit) default `#[requires(true)]`.
-- For writing the postcondition, we use four pieces of Prusti syntax:
-  - [`===`](../syntax.md#snapshot-equality) is called **snapshot equality** or **logical equality**. Is means that the left and right operands are structurally equal. `===` does not require the type of the compared elements to implement [PartialEq](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html), which would be required if we used the standard equality operator `==`.
-  - The [`snap()`](../syntax.md#snap-function) function takes a snapshot of a reference. It has a similar functionality to the [`clone()`](https://doc.rust-lang.org/std/clone/trait.Clone.html) method, but does not require the type of the reference it is called on to implement the `Clone` trait. `snap` should only be used in specifications, since it ignores the borrow checker.
-  - Lastly, we have the [`old()` function](../syntax.md#old-expressions), which denotes that we want to refer to the state of `snap(dest)` from before the function was called.
-  - The identifier [`result`](../syntax.md#result-variable) is used to refer to the return parameter of the function.
-- The postcondition consists of two parts, which can either be written in one condition with `&&`, or in multiple `#[ensures(...)]` annotations like in the example above.
-  - The first condition `snap(dest) === src` means: *After the function returns, the location referenced by `dest` is structurally equal to the parameter `src`*
-  - The second part of the postcondition is `result === old(snap(dest))`. This means: *The `result` returned by the function is structurally equal to the the element that was referenced by `dest` **before** the function was called.*
-
-Since `result` is structurally equal to `dest` from before the function call, Prusti knows that the pure function `len()` called on `result` returns the same value as it would have for `dest`.
-
-
-An important thing to note here is that Prusti does ***not*** check if `replace` actually does what the external specification says it does. `#[extern_spec]` implicitly implies the `#[trusted]` annotation, which means that any postconditions are just accepted and used by Prusti.
-
-### Future
+With this, the first of the three properties of `push` is verified, but we still have two more to prove.
 
-There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate parts of the `extern_spec` syntax.
+## Note about external specifications
 
-There is also work being done for providing external specifications for the Rust standard library. Depending on when you are reading this, the `std::mem::replace` function might be annotated already, in that case this `extern_spec` may not be needed anymore.
-You can track the progress and find some already completed specifications [in this Pull Request](https://github.com/viperproject/prusti-dev/pull/1249).
+Prusti verifies the above implementation of `push`, but this might come as a surprise: the implementation calls the standard library method `std::mem::replace`. How does Prusti know what this method does? Prusti performs *function modular* verification, so calls to other methods only use that method's specifications, and never its implementation (which may not even be available, or may use unsupported features).
 
-Specifications for the standard library should eventually be available in the [prusti-std crate](https://crates.io/crates/prusti-std). Any specifications in this crate will be available by adding it to your project's dependencies.
+The answer is that the `prusti-std` crate provides specifications for *some* of the most common standard library methods, including `std::mem::replace`. In situations where `prusti-std` does not (yet) provide a suitable specification for a method used in the code, an *external specification* must be declared. Creating external specifications is discussed in the [`prusti-std` and External Specifications](extern_specs.md) chapter of this guide.
 
 ## Trusted functions
 
-As mentioned above, `extern_specs` are implicitly `#[trusted]` by Prusti.
+External specifications, like the one for `std::mem::replace` provided by `prusti-std`, are implicitly `#[trusted]` by Prusti.
 Trusted functions can be used for verifying projects containing external code that does not have Prusti annotations, or projects using Rust features that are not yet supported by Prusti.
 An example is printing a string slice (not supported yet):
 ```rust,noplaypen
@@ -156,17 +97,6 @@ This one is even worse, it will enable anything to be verified:
 fn wrong() {}
 ```
 
-### Checking the `extern_spec`
-
-Let's get back to our code. After adding the external specification for `std::mem::replace`, we can finally verify the first property of our `push` function:
-
-```rust,noplaypen
-{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:property_1}}
-// Prusti: Verifies
-```
-
-With this, the first of the three properties of `push` is verified, but we still have two more to prove.
-
 ## Second property
 
 Recall the second property of our specification:
@@ -203,9 +133,6 @@ We don't need to add the condition `0 <= index`, since `index` has the type `usi
 
 After these changes, Prusti can successfully verify the code, so the first two properties of `push` are correct.
 
-
-
-
 ## Third property
 
 The third and final property we will verify for `push` is that the original list
diff --git a/docs/user-guide/src/tour/setup.md b/docs/user-guide/src/tour/setup.md
index ea0e2171e91..74d9fd4d426 100644
--- a/docs/user-guide/src/tour/setup.md
+++ b/docs/user-guide/src/tour/setup.md
@@ -18,10 +18,10 @@ cargo add prusti-contracts
 For older versions of Rust, you can manually add the dependency in your Cargo.toml file:
 ```toml
 [dependencies]
-prusti-contracts = "0.1.6"
+prusti-contracts = "0.1"
 ```
 
-To use prusti-contracts in a Rust code file, just add the following line:
+To use `prusti-contracts` in a Rust code file, just add the following line:
 ```rust,ignore
 use prusti_contracts::*;
 ```
@@ -37,9 +37,9 @@ check_overflows = false
 
 <!-- TODO: link capabilities/limitations chapter (strings) -->
 
-## Standard library annotations
+## Standard library specifications
 
-Annotations for functions and types in the Rust standard library will be available in the [`prusti-std` crate](https://crates.io/crates/prusti-std) after [this PR](https://github.com/viperproject/prusti-dev/pull/1249) is merged.
+Specifications for functions and types in the Rust standard library are provided in the [`prusti-std` crate](https://crates.io/crates/prusti-std).
 
 Adding this crate works the same as for the `prusti-contracts` crate:
 ```sh
@@ -48,6 +48,11 @@ cargo add prusti-std
 or:
 ```toml
 [dependencies]
-prusti-std = "0.1.6"
+prusti-std = "0.1"
+```
+
+To make the specifications available when using `cargo prusti`, the following line also needs to be added to the crate:
+
+```rust,ignore
+use prusti_std;
 ```
-You do not need to import anything to use the annotations in this crate in a file.
diff --git a/docs/user-guide/src/tour/summary.md b/docs/user-guide/src/tour/summary.md
index 2f3c4bd7534..3eb78053031 100644
--- a/docs/user-guide/src/tour/summary.md
+++ b/docs/user-guide/src/tour/summary.md
@@ -49,3 +49,4 @@ are as follows:
 11. [Final Code](final.md): Final code for the verified linked list
 12. [Loop Invariants](loop_invariants.md): Verifying code containing loops by writing loop invariants
 13. [Counterexamples](counterexamples.md): Getting counterexamples for failing assertions
+14. [`prusti-std` and External Specifications](extern_specs.md): Specifications for the Rust standard library, specifying external methods
diff --git a/prusti-contracts/prusti-contracts/src/core_spec/mem.rs b/prusti-contracts/prusti-contracts/src/core_spec/mem.rs
index 21e202d0488..c14919f14b8 100644
--- a/prusti-contracts/prusti-contracts/src/core_spec/mem.rs
+++ b/prusti-contracts/prusti-contracts/src/core_spec/mem.rs
@@ -12,6 +12,10 @@ mod mem {
 
     #[ensures(*x === old(snap(y)) && *y === old(snap(x)))]
     fn swap<T>(x: &mut T, y: &mut T);
+
+    #[ensures(snap(dest) === src)]
+    #[ensures(result === old(snap(dest)))]
+    fn replace<T>(dest: &mut T, src: T) -> T;
 }
 
 pub trait KnownSize {
diff --git a/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs b/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs
index 4302e9cd5b5..c92daa57cb7 100644
--- a/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs
+++ b/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs
@@ -17,32 +17,6 @@ struct Node<T> {
     next: Link<T>,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
 //// ANCHOR: peek_mut_code
 impl<T> List<T> {
     //// ANCHOR_END: peek_mut_code
diff --git a/prusti-tests/tests/verify/fail/user-guide/pop.rs b/prusti-tests/tests/verify/fail/user-guide/pop.rs
index 95c2eec5369..b7426c55ecc 100644
--- a/prusti-tests/tests/verify/fail/user-guide/pop.rs
+++ b/prusti-tests/tests/verify/fail/user-guide/pop.rs
@@ -29,7 +29,7 @@ impl List {
     pub fn len(&self) -> usize {
         self.head.len()
     }
-    
+
     //// ANCHOR: is_empty
     #[pure]
     fn is_empty(&self) -> bool {
@@ -50,7 +50,7 @@ impl List {
         self.head.lookup(index)
     }
 
-    #[ensures(self.len() == old(self.len()) + 1)] //~ ERROR postcondition might not hold
+    #[ensures(self.len() == old(self.len()) + 1)]
     #[ensures(self.lookup(0) == elem)]
     #[ensures(forall(|i: usize| (i < old(self.len())) ==>
                  old(self.lookup(i)) == self.lookup(i + 1)))]
@@ -73,13 +73,13 @@ impl List {
             },
         }
     }
-    
+
     //// ANCHOR_END: initial
     //// ANCHOR: pop_precondition
     #[requires(!self.is_empty())]
     //// ANCHOR: initial
     pub fn pop(&mut self) -> i32 {
-        self.try_pop().unwrap()
+        self.try_pop().unwrap() //~ ERROR precondition might not hold
     }
     //// ANCHOR: is_empty
 }
@@ -99,10 +99,10 @@ impl Link {
                     node.next.lookup(index - 1)
                 }
             },
-            Link::Empty => unreachable!(),  
+            Link::Empty => unreachable!(),
         }
     }
-    
+
     #[pure]
     fn len(&self) -> usize {
         match self {
diff --git a/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs b/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs
index fbbeec1a421..15bb4a4bfd0 100644
--- a/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs
+++ b/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs
@@ -18,11 +18,6 @@ struct Node {
     next: Link,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
 //// ANCHOR: lookup
 impl List {
     #[pure]
diff --git a/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs b/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs
index 1d01faef70b..6ba6a46639d 100644
--- a/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs
@@ -17,32 +17,6 @@ struct Node<T> {
     next: Link<T>,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
 //// ANCHOR: pledge
 impl<T> List<T> {
     //// ANCHOR_END: pledge
diff --git a/prusti-tests/tests/verify/pass/user-guide/generic.rs b/prusti-tests/tests/verify/pass/user-guide/generic.rs
index 8f25ba1da4e..0cf6d00cb93 100644
--- a/prusti-tests/tests/verify/pass/user-guide/generic.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/generic.rs
@@ -20,32 +20,6 @@ struct Node<T> {
 }
 
 //// ANCHOR_END: generic_types
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
 
 //// ANCHOR: generic_types
 //// ANCHOR: lookup_reference
@@ -142,8 +116,8 @@ impl<T> List<T> {
     }
 }
 //// ANCHOR_END: lookup_reference
-
 //// ANCHOR_END: generic_types
+
 #[pure]
 #[requires(index < link_len(link))]
 //// ANCHOR: lookup_reference
@@ -171,13 +145,11 @@ fn link_len<T>(link: &Link<T>) -> usize {
     }
 }
 
-//// ANCHOR: generic_types
 //// ANCHOR: lookup_reference
 #[cfg(prusti)]
 mod prusti_tests {
     use super::*;
 
-    //// ANCHOR_END: generic_types
     fn _test_list(){
         // ...
         //// ANCHOR_END: lookup_reference
@@ -208,5 +180,4 @@ mod prusti_tests {
         //// ANCHOR: lookup_reference
     }
 }
-//// ANCHOR_END: generic_types
 //// ANCHOR_END: lookup_reference
\ No newline at end of file
diff --git a/prusti-tests/tests/verify/pass/user-guide/option.rs b/prusti-tests/tests/verify/pass/user-guide/option.rs
index 48d75f37026..b2e8c4fb3cb 100644
--- a/prusti-tests/tests/verify/pass/user-guide/option.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/option.rs
@@ -17,39 +17,6 @@ struct Node {
     next: Link,
 }
 
-//// ANCHOR: option_take_extern_spec
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-//// ANCHOR_END: option_take_extern_spec
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-//// ANCHOR: option_take_extern_spec
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    //// ANCHOR_END: option_take_extern_spec
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    //// ANCHOR: option_take_extern_spec
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
-//// ANCHOR_END: option_take_extern_spec
-
 //// ANCHOR: try_pop_rewrite
 //// ANCHOR: rewrite_link_impl
 impl List {
@@ -121,7 +88,7 @@ impl List {
         }
     }
     
-    // // This will likely work in the future, but doesn't currently (even if you provide an `extern_spec` for `Option::map`):
+    // // This will likely work in the future, but doesn't currently:
     // // Currently you get this error:
     // //     [Prusti: unsupported feature] unsupported creation of unique borrows (implicitly created in closure bindings)
     // pub fn try_pop(&mut self) -> Option<i32> {
diff --git a/prusti-tests/tests/verify/pass/user-guide/peek.rs b/prusti-tests/tests/verify/pass/user-guide/peek.rs
index a964451fe4e..8cee81dcbfe 100644
--- a/prusti-tests/tests/verify/pass/user-guide/peek.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/peek.rs
@@ -17,33 +17,6 @@ struct Node<T> {
     next: Link<T>,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
-
 //// ANCHOR: implementation
 impl<T> List<T> {
     //// ANCHOR_END: implementation
diff --git a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs
index e083b676514..19d99b3cbc1 100644
--- a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs
@@ -17,32 +17,6 @@ struct Node<T> {
     next: Link<T>,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-
-    #[ensures(result === old(snap(self)))]
-    #[ensures(self.is_none())]
-    pub fn take(&mut self) -> Option<T>;
-}
 //// ANCHOR: pledge
 impl<T> List<T> {
     //// ANCHOR_END: pledge
diff --git a/prusti-tests/tests/verify/pass/user-guide/pop.rs b/prusti-tests/tests/verify/pass/user-guide/pop.rs
index b2026b18b3f..f40290d4d85 100644
--- a/prusti-tests/tests/verify/pass/user-guide/pop.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/pop.rs
@@ -20,31 +20,6 @@ struct Node {
     next: Link,
 }
 
-//// ANCHOR: extern_spec
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-}
-//// ANCHOR_END: extern_spec
-
 //// ANCHOR: two_state_predicate
 //// ANCHOR: predicate_use
 //// ANCHOR: try_pop_empty
diff --git a/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs b/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs
index 30f3e9efaaf..72601b7420f 100644
--- a/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs
@@ -20,11 +20,6 @@ struct Node {
     next: Link,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
 //// ANCHOR: shifted_back
 impl List {
     //// ANCHOR_END: shifted_back
diff --git a/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs b/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs
index 4eb11dd92cb..f0be7f169a1 100644
--- a/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs
@@ -18,13 +18,6 @@ struct Node {
     next: Link,
 }
 
-//// ANCHOR: extern_spec
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-//// ANCHOR_END: extern_spec
-
 //// ANCHOR: property_1
 impl List {
     #[ensures(self.len() == old(self.len()) + 1)] // 1. Property
diff --git a/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs b/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs
index 47c9baeae60..fc54e6663ef 100644
--- a/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs
@@ -18,11 +18,6 @@ struct Node {
     next: Link,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
 //// ANCHOR: bounds
 impl List {
     #[pure]
diff --git a/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs b/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs
index 4e2d1de1b7a..94f6e7dff16 100644
--- a/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs
+++ b/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs
@@ -18,29 +18,6 @@ struct Node {
     next: Link,
 }
 
-#[extern_spec(std::mem)]
-#[ensures(snap(dest) === src)]
-#[ensures(result === old(snap(dest)))]
-fn replace<T>(dest: &mut T, src: T) -> T;
-
-// Specs for std::option::Option<T>::unwrap(self) (and others) can be found here (work in progress):
-// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49
-
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T;
-    
-    #[pure]
-    #[ensures(result == matches!(self, None))]
-    pub const fn is_none(&self) -> bool;
-
-    #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
-}
-
 impl List {
     #[pure]
     pub fn len(&self) -> usize {