diff --git a/refman/.gitignore b/refman/.gitignore
index 829b57d1..cbeb53ce 100644
--- a/refman/.gitignore
+++ b/refman/.gitignore
@@ -6,3 +6,4 @@ lisa.fls
 lisa.log
 lisa.out
 lisa.toc
+src/.scala-build
diff --git a/refman/lisa.pdf b/refman/lisa.pdf
index d22d7da5..a0cf24de 100644
Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ
diff --git a/refman/lisa.tex b/refman/lisa.tex
index 4e6ae055..d52bd948 100644
--- a/refman/lisa.tex
+++ b/refman/lisa.tex
@@ -21,7 +21,8 @@
 \date{}
 
 % PDF links and meta data
-\usepackage{hyperref} 
+%\usepackage{hyperref} 
+\usepackage{bookmark} 
 \makeatletter
 \hypersetup{
     colorlinks=true,
diff --git a/refman/macro.tex b/refman/macro.tex
index 31938969..4a2bf14e 100644
--- a/refman/macro.tex
+++ b/refman/macro.tex
@@ -184,3 +184,6 @@
 
 \DeclareMathOperator{\pick}{pick}
 
+\newcommand{\lisaCode}[3]{
+\lstinputlisting[language=lisa, frame=single,caption=\href{#1}{#2}, #3]{#1}
+}
diff --git a/refman/prooflib.tex b/refman/prooflib.tex
index 7daebca4..47e372f8 100644
--- a/refman/prooflib.tex
+++ b/refman/prooflib.tex
@@ -6,34 +6,7 @@ \chapter{Developping Mathematics with Prooflib}
 \autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in Lisa.
 
 \begin{figure}
-\begin{lstlisting}[language=lisa, frame=single]
-object MyTheoryName extends lisa.Main {
-  val x = variable
-  val f = function[1]
-  val P = predicate[1]
-
-  val fixedPointDoubleApplication = Theorem( 
-    ∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))
-  ) {
-    assume(∀(x, P(x) ==> P(f(x))))
-    val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
-    val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
-    have(thesis) by Tautology.from(step1, step2)
-  } 
-
-  val emptySetIsASubset = Theorem(
-    ∅ ⊆ x
-  ) {
-    have((y ∈ ∅) ==> (y ∈ x)) by Tautology.from(
-                            emptySetAxiom of (x := y))
-    val rhs = thenHave (∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall
-    have(thesis) by Tautology.from(
-                            subsetAxiom of (x := ∅, y := x), rhs)
-  }
-
-}
-\end{lstlisting}
-\caption{An example of a theory file in Lisa}
+\lisaCode{src/MyTheoryName.scala}{An example of a theory file in Lisa}{firstline=3}
 \label{fig:theoryFileExample}
 \end{figure}
 
diff --git a/refman/src/MyTheoryName.scala b/refman/src/MyTheoryName.scala
new file mode 100644
index 00000000..b2a48eb4
--- /dev/null
+++ b/refman/src/MyTheoryName.scala
@@ -0,0 +1,29 @@
+//> using scala 3.5.1
+//> using jar "../../../lisa/target/scala-3.5.1/lisa-assembly-0.7.jar"
+object MyTheoryName extends lisa.Main:
+  val x = variable
+  val y = variable
+  val f = function[1]
+  val P = predicate[1]
+
+  val fixedPointDoubleApplication = Theorem( 
+    ∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))
+  ) {
+    assume(∀(x, P(x) ==> P(f(x))))
+    val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
+    val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
+    have(thesis) by Tautology.from(step1, step2)
+  } 
+
+  val emptySetIsASubset = Theorem(
+    ∅ ⊆ x
+  ) {
+    have((y ∈ ∅) ==> (y ∈ x)) by Tautology.from(
+                            emptySetAxiom of (x := y))
+    val rhs = thenHave (∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall
+    have(thesis) by Tautology.from(
+                            subsetAxiom of (x := ∅, y := x), rhs)
+  }
+
+  @main def show = println(emptySetAxiom)
+