diff --git a/trees/index.tree b/trees/index.tree
index 26b6dd4..6496215 100644
--- a/trees/index.tree
+++ b/trees/index.tree
@@ -8,7 +8,7 @@
 \put\transclude/heading{true}
 \transclude{loc-000E}
 \subtree{\title{Lecture notes}
-\p{[[dt-001Y]]}
+\ul{\li{[[dt-001Y]]} \li{[[isa-0001]]}}
 }
 \transclude{news}
 }
diff --git a/trees/isa/isa-0001.tree b/trees/isa/isa-0001.tree
index 16ee571..d162daf 100644
--- a/trees/isa/isa-0001.tree
+++ b/trees/isa/isa-0001.tree
@@ -1,4 +1,4 @@
-\title{Introduction to Interactive Theorem Proving (Draft)}
+\title{Interactive theorem proving (draft)}
 \author{liamoc}
 \taxon{Lecture Notes}
 \p{These notes are the basis of my short course at the [ANU Logic Summer School]() 2025. \strong{THEY ARE NOT YET COMPLETE.}}
diff --git a/trees/isa/isa-001B.tree b/trees/isa/isa-001B.tree
index 5bf68da..69debb0 100644
--- a/trees/isa/isa-001B.tree
+++ b/trees/isa/isa-001B.tree
@@ -32,3 +32,40 @@ thm ssubst}
 \transclude{isa-001J}
 \transclude{isa-001L}
 \transclude{isa-001M}
+\ul{
+  \li{natural numbers}
+  \li{Fun command}
+  \li{rpt}
+  \li{induct method (structural)}
+  \li{rpt twice theorem}
+  \li{twos type}  
+  \li{prepend}
+  \li{prepend prepend theorem}
+  \li{semicolon operator}
+  \li{append}  
+  \li{append prepend theorem}
+  \li{append assoc}
+  \li{lists (replicate function)}
+  \li{decompress}
+  \li{compress}
+  \li{decompress compress thm}
+  \li{compress app}
+  \li{compress replicate}
+  \li{inductive predicates}
+  \li{rule induction}
+  \li{wellformedness}
+  \li{compress decompress thm}
+  \li{arbitrary}
+  \li{chaining}
+  \li{repeating}
+  \li{subsequence example}
+  \li{subsequence theorems}
+  \li{safe vs unsafe rules}
+  \li{intro, elim, clarify, blast, (fast,slow,best)}}
+  \li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force}
+  \li{sledgehammer, try, find_theorems}
+  \li{clarify, clarsimp}
+  \li{structured proofs}
+  \li{calculational proofs}
+  \li{examples examples examples}
+}
\ No newline at end of file