diff --git a/dicts/dicts.gobra b/dicts/dicts.gobra
index bcbf125..ec11546 100644
--- a/dicts/dicts.gobra
+++ b/dicts/dicts.gobra
@@ -13,6 +13,7 @@
     - https://www.why3.org/stdlib/fmap.html
     - https://www.why3.org/stdlib/map.html
 */
+//+gobra
 
 // This package defines lemmas for mathematical maps (aka dictionaries) commonly used
 // in specifications.
diff --git a/gomap/gomap.gobra b/gomap/gomap.gobra
index fc92223..c940dd7 100644
--- a/gomap/gomap.gobra
+++ b/gomap/gomap.gobra
@@ -3,6 +3,7 @@
   See LICENSE or go to https://github.com/viperproject/gobra-libs/blob/main/LICENSE
   for full license details.
 */
+//+gobra
 
 // This package defines Go maps and their associated operations in terms of
 // mathematical maps (dictionaries).
diff --git a/math/math.gobra b/math/math.gobra
index 1b1e478..bb242e9 100644
--- a/math/math.gobra
+++ b/math/math.gobra
@@ -1,3 +1,4 @@
+//+gobra
 // This package defines mathematical operations commonly used in specifications.
 package math
 
diff --git a/seqs/seqs.gobra b/seqs/seqs.gobra
index 4ee8d6a..3031acf 100644
--- a/seqs/seqs.gobra
+++ b/seqs/seqs.gobra
@@ -6,6 +6,7 @@
   This file is inspired by the standard libraries and axiomatisations of the following verifiers:
   - dafny-lang/libraries: https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy
 */
+//+gobra
 
 // This package defines lemmas for sequences commonly used in specifications.
 package seqs
diff --git a/sets/sets.gobra b/sets/sets.gobra
index c001f12..cb00302 100644
--- a/sets/sets.gobra
+++ b/sets/sets.gobra
@@ -10,6 +10,7 @@
   - viperproject/silicon: https://github.com/viperproject/silicon/blob/master/src/main/resources/dafny_axioms/sets.vpr
 
 */
+//+gobra
 
 // This package defines lemmas for sets commonly used in specifications.
 package sets
diff --git a/util/util.gobra b/util/util.gobra
index 007849f..b8b26b2 100644
--- a/util/util.gobra
+++ b/util/util.gobra
@@ -12,6 +12,7 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//+gobra
 package util
 
 type Unit struct{}
@@ -50,4 +51,4 @@ requires b
 decreases
 pure func Asserting(ghost b bool) Unit {
 	return Unit{}
-}
\ No newline at end of file
+}