diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
index 46d8851..30d6f70 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
@@ -35,7 +35,7 @@ namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is
-  the algebra is generated by creation and annihilation parts of field operators defined in
+  the algebra generated by creation and annihilation parts of field operators defined in
   `𝓕.CrAnFieldOp`.
   It represents the algebra containing all possible products and linear combinations
   of creation and annihilation parts of field operators, without imposing any conditions.
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index a3b6471..2792bfa 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -147,34 +147,43 @@ def perturbationTheory : Note where
     .name `FieldSpecification.CrAnFieldOp,
     .h2 "Field-operator free algebra",
     .name `FieldSpecification.FieldOpFreeAlgebra,
+    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
     .h2 "Field-operator algebra",
     .name `FieldSpecification.FieldOpAlgebra,
+    .name `FieldSpecification.FieldOpAlgebra.superCommute,
     .h1 "Time ordering",
-    .name `FieldSpecification.timeOrderRel,
-    .name `FieldSpecification.timeOrderSign,
+    .name `FieldSpecification.crAnTimeOrderRel,
+    .name `FieldSpecification.crAnTimeOrderSign,
+    .name `FieldSpecification.FieldOpFreeAlgebra.timeOrderF,
+    .name `FieldSpecification.FieldOpAlgebra.timeOrder,
     .h1 "Normal ordering",
+    .name `FieldSpecification.normalOrderRel,
+    .name `FieldSpecification.normalOrderSign,
+    .name `FieldSpecification.FieldOpFreeAlgebra.normalOrderF,
+    .name `FieldSpecification.FieldOpAlgebra.normalOrder,
     .h1 "Wick Contractions",
     .h2 "Definition",
+    .name `WickContraction,
+    .name `WickContraction.GradingCompliant,
     .h2 "Constructors",
     .p "There are a number of ways to construct a Wick contraction from
       other Wick contractions or single contractions.",
+    .name `WickContraction.insertAndContract,
+    .name `WickContraction.erase,
+    .name `WickContraction.join,
     .h2 "Sign",
-    .h1 "Static Wick's theorem",
-    .h1 "Time-dependent Wick's theorem",
-    .h2 "Wick terms",
-    .name `FieldSpecification.wick_term_terminology,
-    .name `FieldSpecification.wick_term_none_eq_wick_term_cons,
-    .name `FieldSpecification.wick_term_some_eq_wick_term_optionEraseZ,
-    .name `FieldSpecification.wick_term_cons_eq_sum_wick_term,
-    .h2 "The case of the nil list",
-    .p "Our proof of Wick's theorem will be via induction on the number of fields that
-      are in the time-ordered product. The base case is when there are no fields.
-      The proof of Wick's theorem follows from definitions and simple lemmas.",
-    .name `FieldSpecification.wicks_theorem_nil,
-    .h2 "Wick's theorems",
+    .name `WickContraction.sign,
+    .name `WickContraction.signInsertNone_eq_filterset,
+    .name `WickContraction.signInsertSome_mul_filter_contracted_of_not_lt,
+    .name `WickContraction.join_sign,
+    .h2 "Cardinality",
+    .name `WickContraction.card_eq_cardFun,
+    .h1 "Time and static contractions",
+    .h1 "The three Wick's theorems",
     .name `FieldSpecification.wicks_theorem,
-    .h1 "Wick's theorem with normal ordering"]
-
+    .name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,
+    .name `FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order
+    ]
 
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)