diff --git a/docs/src/concepts/symbolic_models.md b/docs/src/concepts/symbolic_models.md
index 50785f14..d29bdd73 100644
--- a/docs/src/concepts/symbolic_models.md
+++ b/docs/src/concepts/symbolic_models.md
@@ -16,7 +16,7 @@ To get started, you can always call the `@symbolic_model` macro with an empty bo
 Below, we subtype from GATlab's abstract types `ObExpr` and `HomExpr` to enable
 LaTeX pretty-printing and other convenient features, but this is not required.
 
-```@example category
+```julia
 @symbolic_model CategoryExprs{ObExpr, HomExpr} ThCategory begin
 end
 A, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]
@@ -27,7 +27,7 @@ compose(compose(f,g),h)
 The resulting symbolic expressions perform no simplification. For example, the
 associativity law is not satisfied:
 
-```@example category
+```julia
 compose(compose(f,g),h) == compose(f,compose(g,h))
 ```
 
@@ -36,12 +36,12 @@ obey all the axioms of the theory.
 
 However, the user may supply logic in the body of the `@symbolic_model` macro to enforce
 the axioms or perform other kinds of simplification. Below, we use the
-[`associate`](@ref) function provided by GATlab to convert the binary
+`associate` function provided by GATlab to convert the binary
 expressions representing composition into $n$-ary expressions for any number
 $n$. The option `strict=true` tells GATlab to check that the domain and codomain
 objects are strictly equal and throw an error if they are not.
 
-```@example category
+```julia
 @symbolic_model SimplifyingCategoryExprs{ObExpr, HomExpr} ThCategory begin
   compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
 end
@@ -52,7 +52,7 @@ compose(compose(f,g),h)
 
 Now the associativity law *is* satisfied:
 
-```@example category
+```julia
 compose(compose(f,g),h) == compose(f,compose(g,h))
 ```
 
@@ -73,11 +73,11 @@ determine which operations, if any, will be derived from others. In the case of
 the cartesian monoidal category, we could define a signature `CartesianCategory`
 by inheriting from the builtin theory `SymmetricMonoidalCategory`.
 
-```@setup cartesian-monoidal-category
+```julia
 using GATlab
 ```
 
-```@example cartesian-monoidal-category
+```julia
 @signature ThCartesianCategory <: ThSymmetricMonoidalCategory begin
   mcopy(A::Ob)::(A → (A ⊗ A))
   delete(A::Ob)::(A → munit())
@@ -90,7 +90,7 @@ nothing # hide
 
 We could then define the copying operation in terms of the pairing.
 
-```@example cartesian-monoidal-category
+```julia
 @symbolic_model CartesianCategoryExprsV1{ObExpr,HomExpr} ThCartesianCategory begin
   mcopy(A::Ob) = pair(id(A), id(A))
 end
@@ -101,7 +101,7 @@ mcopy(A)
 Alternatively, we could define the pairing and projections in terms of the
 copying and deleting operations.
 
-```@example cartesian-monoidal-category
+```julia
 @symbolic_model CartesianCategoryExprsV2{ObExpr,HomExpr} ThCartesianCategory begin
   pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))
   proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))
diff --git a/docs/src/concepts/theories.md b/docs/src/concepts/theories.md
index ffcb41d1..3dbd9c08 100644
--- a/docs/src/concepts/theories.md
+++ b/docs/src/concepts/theories.md
@@ -59,7 +59,7 @@ algebra, thus, providing a perfect opportunity for computer algebra systems.
 
 GATlab implements a version of the GAT formalism on top of Julia's type system,
 taking advantage of Julia macros to provide a pleasant syntax. GATs are defined
-using the [`@theory`](@ref) macro.
+using the `@theory` macro.
 
 For example, the theory of categories could be defined by: