Remove comment, fix some formatting

source/docs/guide/src/integers.md

@@ -27,16 +27,6 @@ a `u8` value is an integer constrained to be greater than or equal to `0` and le
 {{#include ../../../rust_verify/example/guide/integers.rs:test_u8}}
 ```
 
-<!-- (The bounds of `usize` and `isize` are platform dependent.
-By default, Verus assumes that these types may be either 32 bits or 64 bits wide,
-but this can be configured with the directive:
-
-```rust
-global size_of usize == 8;
-```
-
-(This would set the size of `usize` to 8 bytes, and add a static assertion to check it matches the target.) -->
-
 # Using integer types in specifications
 
 Since there are 14 different integer types (counting `int`, `nat`, `u8`...`usize`, and `i8`...`isize`),

source/docs/guide/src/sized.md

@@ -2,7 +2,6 @@
 
 Verus does not have direct access to the result of `core::mem::size_of<T>()` during verification. The size of most types is undefined by default (with the exception of `usize`/`isize`; see below). To use the size of `Sized` types in spec code, the `global size_of` directive may be used to set the size of the type and add a static assertion for the Rust compiler to check that the provided size matches the result of `core::mem::size_of<T>()`. Note that checking this assertion requires the `--compile` flag, as the assertion is checked by Rust, not Verus.
 
-
 For example:
 
 ```rust