Remove import <decreases/*.vpr>

It is no longer needed since release 2023.7 to import, they are imported
automatically.

Signed-off-by: Samuel Tyler <samuel@samuelt.me>

Author: fosslinux

src/termination-conditional.md

@@ -18,8 +18,6 @@ Here, `<condition>` is a boolean expression under which the decreases clause is
 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.
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-
 function sign(x: Int): Int
   decreases x if 1 <= x
   decreases _ if x <= -1

src/termination-custom-orders.md

@@ -5,8 +5,6 @@ As previously mentioned, Viper offers [predefined orders](./termination-measures
 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.
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-
 domain MyInt {
   function put(i: Int): MyInt   // Constructor
   function get(m: MyInt): Int   // Destructor

src/termination-measures.md

@@ -11,8 +11,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.
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-
 function factorial(n:Int) : Int
   requires 0 <= n
   decreases n
@@ -25,7 +23,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 |
 | ---- | ---- |
@@ -44,8 +42,6 @@ All definitions are straightforward, except the last one, which is concerned wit
 Viper uses this nesting depth 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)`.
 
 ```viper,editable,playground
-import <decreases/predicate_instance.vpr>
-
 field next: Ref
 
 predicate list(this: Ref) {

src/termination-mutual-recursion.md

@@ -5,8 +5,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`:
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-
 function is_even(x: Int): Bool
   requires x >= 0
   decreases x
@@ -27,9 +25,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):
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-import <decreases/bool.vpr>
-
 function fun1(y: Int, b: Bool): Int
   decreases y, b
 {

src/termination-statement.md

@@ -59,8 +59,6 @@ The currently implemented approach to checking termination of methods is similar
 A straightforward example is method `sum`, shown next:
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-
 method sum(n: Int) returns (res: Int)
   requires 0 <= n
   decreases

src/termination-syntax.md

@@ -15,8 +15,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:
 
 ```viper,editable,playground
-import <decreases/int.vpr>
-
 function ack(m:Int, n:Int):Int
   decreases m, n
   requires m >= 0