diff --git a/tutorial/termination.md b/tutorial/termination.md
index bd4326a..7e3a374 100644
--- a/tutorial/termination.md
+++ b/tutorial/termination.md
@@ -23,8 +23,6 @@ Here, `<tuple>` denotes the termination measure: a tuple of comma-separated expr
 A common example for termination is the standard `factorial` function, which terminates because its argument decreases with respect to the usual well-founded order over non-negative numbers.
 
 ```silver-runnable
-import <decreases/int.vpr>
-
 function factorial(n:Int) : Int
   requires 0 <= n
   decreases n
@@ -37,7 +35,7 @@ Viper successfully verifies that `factorial` terminates: at each recursive invoc
 
 ### Predefined Well-Founded Orders {#term_prov_wfo}
 
-Viper's standard library provides definitions of well-founded orders for most types built into Viper, all of which can be imported from the `decreases` folder. The following table lists all provided orders; we write `s1 <_ s2` if `s1` is less than `s2` with respect to the order.
+Viper's standard library provides definitions of well-founded orders for most types built into Viper. They are automatically imported upon use of a `decreases` statement. Alternatively, they can also be imported from the `decreases` folder. The following table lists all provided orders; we write `s1 <_ s2` if `s1` is less than `s2` with respect to the order.
 
 | Build-In Type<br>(file name) | Provided Well-Founded Order |
 | ---- | ---- |
@@ -56,8 +54,6 @@ All definitions are straightforward, except the last one, which is concerned wit
 Viper uses this nesting relation to enable termination checks based on predicate instances, as illustrated by the next example, the recursive computation of the length of a linked list: intuitively, the remainder of the linked list, represented by predicate instance `list(this)`, is used as the termination measure. This works because the recursive call is nested under the unfolding of `list(this)`, and takes the smaller predicate instance `list(this.next)`.
 
 ```silver-runnable
-import <decreases/predicate_instance.vpr>
-
 field next: Ref
 
 predicate list(this: Ref) {
@@ -100,8 +96,6 @@ Special cases, such as empty tuples, tuples of different length, and tuples of d
 A typical example of a function for which a tuple as termination measure is used, is the Ackermann function:
 
 ```silver-runnable
-import <decreases/int.vpr>
-
 function ack(m:Int, n:Int):Int
   decreases m, n
   requires m >= 0
@@ -189,8 +183,6 @@ As previously mentioned, Viper offers [predefined orders](#term_prov_wfo) for it
 In the remainder of this subsection, both approaches will be illustrated using a combination of the `MyInt` example (from the earlier subsection on domains) and a `factorial` function operating on `MyInt`. In the example below, the destructor `get` is used to map a `MyInt` to a regular `Int`, which indirectly allows using `MyInt` in the function's decreases clause.
 
 ```silver-runnable
-import <decreases/int.vpr>
-
 domain MyInt {
   function put(i: Int): MyInt   // Constructor
   function get(m: MyInt): Int   // Destructor
@@ -257,8 +249,6 @@ For mutually recursive functions, Viper implements the following approach (as, e
 A simple case of mutual recursion is illustrated next, by functions `is_even` and `is_odd`:
 
 ```silver-runnable
-import <decreases/int.vpr>
-
 function is_even(x: Int): Bool
   requires x >= 0
   decreases x
@@ -279,9 +269,6 @@ Consider function `is_even`: its termination measure `x` decreases at the indire
 In the example above, the two termination measures are tuples of equal length and type. However, this is not required of mutually recursive functions in order to prove their termination. Consider the next example (which verifies successfully):
 
 ```silver-runnable
-import <decreases/int.vpr>
-import <decreases/bool.vpr>
-
 function fun1(y: Int, b: Bool): Int
   decreases y, b
 {
@@ -326,8 +313,6 @@ To ensure soundness, only a *single* clause per kind of measure is allowed. More
 The following example illustrates combined conditional termination clauses: function `sign` promises to decrease `x` if positive, and something (wildcard) if `x` is negative. In case `x` is zero, function `sign` does not (promise to) terminate.
 
 ```silver-runnable
-import <decreases/int.vpr>
-
 function sign(x: Int): Int
   decreases x if 1 <= x
   decreases _ if x <= -1
@@ -431,8 +416,6 @@ The currently implemented approach to checking termination of methods is similar
 A straightforward example is method `sum`, shown next:
 
 ```silver-runnable
-import <decreases/int.vpr>
-
 method sum(n: Int) returns (res: Int)
   requires 0 <= n
   decreases