diff --git a/trees/isa/isa-0001.tree b/trees/isa/isa-0001.tree
index d162daf..5d5816f 100644
--- a/trees/isa/isa-0001.tree
+++ b/trees/isa/isa-0001.tree
@@ -4,3 +4,4 @@
 \p{These notes are the basis of my short course at the [ANU Logic Summer School]() 2025. \strong{THEY ARE NOT YET COMPLETE.}}
 \transclude{isa-0002}
 \transclude{isa-001B}
+\transclude{isa-002N}
diff --git a/trees/isa/isa-001B.tree b/trees/isa/isa-001B.tree
index 346cb8f..9037d4b 100644
--- a/trees/isa/isa-001B.tree
+++ b/trees/isa/isa-001B.tree
@@ -50,25 +50,3 @@ thm ssubst}
 \transclude{isa-0025}
 \transclude{isa-0026}
 \transclude{isa-0027}
-\transclude{isa-0028}
-\transclude{isa-002A}
-\transclude{isa-0029}
-\transclude{isa-002B}
-\transclude{isa-002C}
-\transclude{isa-002D}
-\transclude{isa-002E}
-\transclude{isa-002F}
-\transclude{isa-002G}
-\transclude{isa-002H}
-\transclude{isa-002I}
-\transclude{isa-002J}
-\ul{
-  \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
diff --git a/trees/isa/isa-0028.tree b/trees/isa/isa-0028.tree
index b15ae5d..a43f8e9 100644
--- a/trees/isa/isa-0028.tree
+++ b/trees/isa/isa-0028.tree
@@ -1,4 +1,6 @@
 \date{2025-12-03T06:13:19Z}
 \author{liamoc}
 \title{\code{inductive} predicates}
-\p{TODO}
\ No newline at end of file
+\p{With the \code{inductive} command, we define a predicate by specifying a collection of inference rules, and the inductive predicate is the smallest predicate closed under those rules.}
+\p{In other words: An element satisfies the predicate exactly if it can be derived using the given rules.}
+\p{From the given rules, Isabelle automatically generates an induction principle (\code{.induct}) which can be used with the \code{induct} method (see \ref{isa-0029}) and a cases theorem (\code{.cases}) for use with the [[isa-001L]] method. }
\ No newline at end of file
diff --git a/trees/isa/isa-0029.tree b/trees/isa/isa-0029.tree
index 6442863..0c656ca 100644
--- a/trees/isa/isa-0029.tree
+++ b/trees/isa/isa-0029.tree
@@ -1,5 +1,12 @@
 \date{2025-12-03T06:14:12Z}
 \author{liamoc}
 \taxon{Proof Method}
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
 \title{\code{induct} (for rule induction)}
-\p{TODO}
\ No newline at end of file
+\p{You’ve already seen [how to use \code{induct}](isa-001P) for structural induction. Exactly the same \code{induct} method can also be used for rule induction, when your induction is over an \code{inductive}ly defined predicate, not over the structure of some \code{datatype}.}
+\p{When you define a predicate \code{p} with the [\code{inductive} command](isa-0028), Isabelle automatically produces an induction rule named \code{p.induct}. This rule expresses how to perform induction over derivations of \code{p x}, one case for each introduction rule of the predicate.}
+\p{Although you could apply the raw rule with \code{rule} or \code{erule}, it is almost always easier to use:}
+\shiki{apply (induct rule: p.induct)}
+\p{This behaves just like structural induction:
+The goal is split into one subgoal per introduction rule of the predicate, and recursive premises of the rules give rise to induction hypotheses, added to your assumptions.}
\ No newline at end of file
diff --git a/trees/isa/isa-002B.tree b/trees/isa/isa-002B.tree
index 1bccece..ad757ab 100644
--- a/trees/isa/isa-002B.tree
+++ b/trees/isa/isa-002B.tree
@@ -4,7 +4,7 @@
 \import{dt-macros}
 \put\shiki/language{Isabelle Theory}
 \author{liamoc}
-\parent{isa-001B}
+\parent{isa-002N}
 \title{\code{compress_expand}}
 \shiki{lemma compress_expand:‹well s ⟹ compress (expand s) = s›}
 \solnblock{\shiki{apply (induct rule: well.induct)
diff --git a/trees/isa/isa-002C.tree b/trees/isa/isa-002C.tree
index cbcf32b..732fab6 100644
--- a/trees/isa/isa-002C.tree
+++ b/trees/isa/isa-002C.tree
@@ -1,7 +1,7 @@
 \date{2025-12-03T06:30:43Z}
 \author{liamoc}
 \taxon{Definition}
-\parent{isa-001B}
+\parent{isa-002N}
 \import{shiki-macros}
 \put\shiki/language{Isabelle Theory}
 \title{List subsequence relation}
diff --git a/trees/isa/isa-002D.tree b/trees/isa/isa-002D.tree
index b1e09e9..6a195a5 100644
--- a/trees/isa/isa-002D.tree
+++ b/trees/isa/isa-002D.tree
@@ -4,7 +4,7 @@
 \import{dt-macros}
 \put\shiki/language{Isabelle Theory}
 \author{liamoc}
-\parent{isa-001B}
+\parent{isa-002N}
 \title{Reflexivity of \code{subsequence}}
 \shiki{lemma ss_refl: ‹subsequence ls ls›}
 \solnblock{\shiki{apply (induct ls)
diff --git a/trees/isa/isa-002E.tree b/trees/isa/isa-002E.tree
index 0aab6da..c3d2711 100644
--- a/trees/isa/isa-002E.tree
+++ b/trees/isa/isa-002E.tree
@@ -4,7 +4,7 @@
 \import{dt-macros}
 \put\shiki/language{Isabelle Theory}
 \author{liamoc}
-\parent{isa-001B}
+\parent{isa-002N}
 \title{Length of \code{subsequence}}
 \shiki{lemma ss_length : ‹subsequence xs ys ⟹ length xs ≤ length ys›}
 \solnblock{\shiki{apply (induct rule: subsequence.induct)
diff --git a/trees/isa/isa-002F.tree b/trees/isa/isa-002F.tree
index 0aac458..cb0451c 100644
--- a/trees/isa/isa-002F.tree
+++ b/trees/isa/isa-002F.tree
@@ -1,4 +1,17 @@
 \date{2025-12-03T06:41:41Z}
 \title{Controlling backtracking, chaining methods with comma}
 \author{liamoc}
-\p{TODO}
\ No newline at end of file
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
+\p{Some methods (like [\code{erule}](isa-0011) when there are multiple matching assumptions) are \em{nondeterministic}, producing multiple alternative proof states.}
+\p{The \code{back} command interactively explores a different alternative branch produced by the previous step.}
+\shiki{lemma "C ∧ D ⟹ A ∧ B ⟹ A"
+apply (erule conjE) (* could apply to either assumption *)
+back
+apply assumption
+done}
+\p{This is useful for interactive exploration, but is \em{very brittle} and considered poor style.}
+\p{Instead, we can combine methods with the \em{comma} operator \code{,}: The command \code{apply (m1, m2)} first runs \code{m1}, and then runs \code{m2}, accepting only the nondeterministic branches where the second method \code{m2} succeeds. This avoids the need for back:}
+\shiki{lemma "C ∧ D ⟹ A ∧ B ⟹ A"
+apply (erule conjE, assumption)
+done}
\ No newline at end of file
diff --git a/trees/isa/isa-002G.tree b/trees/isa/isa-002G.tree
index dfe69ed..a8a284f 100644
--- a/trees/isa/isa-002G.tree
+++ b/trees/isa/isa-002G.tree
@@ -1,4 +1,8 @@
 \date{2025-12-03T06:42:16Z}
 \title{Repeating methods with \code{+}}
 \author{liamoc}
-\p{TODO}
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
+\p{For a method \code{m}:}
+\shiki{apply (m)+}
+\p{Repeatedly applies the \code{m} as many times as possible until it fails. It stops automatically when \code{m} can no longer make progress; and does not backtrack.}
diff --git a/trees/isa/isa-002H.tree b/trees/isa/isa-002H.tree
index 78765a8..855ce54 100644
--- a/trees/isa/isa-002H.tree
+++ b/trees/isa/isa-002H.tree
@@ -4,15 +4,15 @@
 \import{dt-macros}
 \put\shiki/language{Isabelle Theory}
 \author{liamoc}
-\parent{isa-001B}
+\parent{isa-002N}
 \title{Antisymmetry of \code{subsequence}}
 \shiki{lemma ss_antisym: ‹subsequence ys xs ⟹ subsequence xs ys ⟹ xs = ys›}
 \solnblock{\shiki{apply (induct rule: subsequence.induct)
   apply simp
  apply simp
- apply (erule subsequence.cases, clarsimp, clarsimp,clarsimp)
+ apply (erule subsequence.cases, simp, simp, simp)
  apply (drule ss_length)+
- apply simp
+apply (drule sym, simp)
  apply (drule ss_length)+
 apply simp
 done}}
diff --git a/trees/isa/isa-002I.tree b/trees/isa/isa-002I.tree
index 18fc726..d81929c 100644
--- a/trees/isa/isa-002I.tree
+++ b/trees/isa/isa-002I.tree
@@ -1,4 +1,9 @@
 \date{2025-12-03T06:48:06Z}
 \author{liamoc}
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
 \title{Generalising the induction hypothesis with \code{arbitrary}}
-\p{TODO}
\ No newline at end of file
+\p{By default, [structural induction](isa-001P) \code{induct t} produces an induction hypothesis for the variables directly mentioned in \code{t}, and [rule induction](isa-0029) \code{induct rule: p.induct} produces a hypothesis for the variables directly mentioned by the eliminated \code{p} assumption.}
+\p{Sometimes you need a stronger hypothesis that generalises across additional variables in the goal. The \code{arbitrary} option tells the \code{induct} method to generalise certain variables, so the induction hypothesis assumes the property holds for all values of those variables.}
+
+\transclude{isa-002M}
\ No newline at end of file
diff --git a/trees/isa/isa-002J.tree b/trees/isa/isa-002J.tree
index e89e1e3..8cd16f5 100644
--- a/trees/isa/isa-002J.tree
+++ b/trees/isa/isa-002J.tree
@@ -4,7 +4,7 @@
 \import{dt-macros}
 \put\shiki/language{Isabelle Theory}
 \author{liamoc}
-\parent{isa-001B}
+\parent{isa-002N}
 \title{Transitivity of \code{subsequence}}
 \shiki{lemma ss_trans: ‹subsequence ys zs ⟹ subsequence xs ys ⟹ subsequence xs zs›}
 \solnblock{\shiki{apply (induct ys zs arbitrary: xs rule: subsequence.induct)
diff --git a/trees/isa/isa-002K.tree b/trees/isa/isa-002K.tree
new file mode 100644
index 0000000..face289
--- /dev/null
+++ b/trees/isa/isa-002K.tree
@@ -0,0 +1,10 @@
+\date{2025-12-03T11:17:28Z}
+\author{liamoc}
+\taxon{Example}
+\import{shiki-macros}
+\parent{isa-002N}
+\title{Even numbers as an \code{inductive}}
+\put\shiki/language{Isabelle Theory}
+\shiki{inductive even :: "nat ⇒ bool" where
+  even0:  "even 0"
+| evenSS: "even n ⟹ even (Suc (Suc n))"}
diff --git a/trees/isa/isa-002L.tree b/trees/isa/isa-002L.tree
new file mode 100644
index 0000000..d02ade4
--- /dev/null
+++ b/trees/isa/isa-002L.tree
@@ -0,0 +1,17 @@
+\date{2025-12-03T11:17:28Z}
+\author{liamoc}
+\taxon{Exercise}
+\import{shiki-macros}
+\import{dt-macros}
+\parent{isa-002N}
+\title{Even numbers are multiples of two}
+\put\shiki/language{Isabelle Theory}
+\shiki{lemma "even n ⟹ ∃m. (m * 2 = n)"}
+\solnblock{
+  \shiki{apply (induct rule: even.induct)
+ apply simp
+apply (erule exE)
+apply (rule_tac x = ‹Suc m› in exI)
+apply simp
+done}}
+
diff --git a/trees/isa/isa-002M.tree b/trees/isa/isa-002M.tree
new file mode 100644
index 0000000..955eb6c
--- /dev/null
+++ b/trees/isa/isa-002M.tree
@@ -0,0 +1,15 @@
+\date{2025-12-03T12:43:00Z}
+\author{liamoc}
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
+\taxon{Example}
+\title{Inequality as an \code{inductive}}
+\shiki{inductive myLE :: "nat ⇒ nat ⇒ bool" where
+  base: "myLE 0 n"
+| step: "myLE m n ⟹ myLE (Suc m) (n+1)"}
+\p{Proving that this implies the normal inequality relation requires the use of [variable generalising](isa-002I):}
+\shiki{lemma "myLE m n ⟹ m ≤ n"
+apply (induct m arbitrary: n)
+ apply simp
+apply (erule myLE.cases; simp)
+done}
\ No newline at end of file
diff --git a/trees/isa/isa-002N.tree b/trees/isa/isa-002N.tree
new file mode 100644
index 0000000..dace466
--- /dev/null
+++ b/trees/isa/isa-002N.tree
@@ -0,0 +1,31 @@
+\date{2025-12-03T12:50:18Z}
+\author{liamoc}
+\taxon{Lecture}
+\title{Rule Induction, Automation, Structured Proofs}
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
+\p{This lecture continues the theory file begun in \ref{isa-001B}.}
+\transclude{isa-0028}
+\transclude{isa-002K}
+\transclude{isa-0029}
+\transclude{isa-002L}
+\transclude{isa-002A}
+\transclude{isa-002B}
+\transclude{isa-002C}
+\transclude{isa-002D}
+\transclude{isa-002E}
+\transclude{isa-002F}
+\transclude{isa-002G}
+\transclude{isa-002H}
+\transclude{isa-002I}
+\transclude{isa-002J}
+\ul{
+  \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