diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k
index d5321436a09..97be6dd994d 100644
--- a/k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k
+++ b/k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k
@@ -1,5 +1,9 @@
// Copyright (c) K Team. All Rights Reserved.
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
require "substitution.md"
module LAMBDA
diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k
index 5f5dec6bcda..ea120a67caa 100644
--- a/k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k
+++ b/k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k
@@ -1,5 +1,9 @@
// Copyright (c) K Team. All Rights Reserved.
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
require "substitution.md"
module LAMBDA
diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k
index 2a6009f34a6..4e6c2558c35 100644
--- a/k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k
+++ b/k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k
@@ -1,5 +1,9 @@
// Copyright (c) K Team. All Rights Reserved.
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
require "substitution.md"
module LAMBDA
diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k
index ff09a894ab2..207bd60f618 100644
--- a/k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k
+++ b/k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k
@@ -1,5 +1,9 @@
// Copyright (c) K Team. All Rights Reserved.
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses substitution, unification and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
require "unification.k"
require "substitution.md"
diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k
index 0d6dba1770f..1cf1cf4f033 100644
--- a/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k
+++ b/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k
@@ -1,5 +1,9 @@
// Copyright (c) K Team. All Rights Reserved.
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both unification and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
require "unification.k"
module LAMBDA
diff --git a/web/pages/index.md b/web/pages/index.md
index 856c99d10c8..07fd8c62480 100644
--- a/web/pages/index.md
+++ b/web/pages/index.md
@@ -27,7 +27,6 @@ call/cc.
## Learn K
- Do the K Tutorial!
-- Build programming languages in K!
- Reference Documentation
- K Cheat Sheet
- K Tool Reference
@@ -41,6 +40,7 @@ call/cc.
## Resources
+- A set of reference implementations and tutorials for common programming language features and paradigms is available, although parts of these implementations may not be fully up to date with modern K features.
- Read some papers about K on the [Formal Systems Laboratory (FSL)](https://fsl.cs.illinois.edu/publications/).
- [Matching logic](http://matching-logic.org/) webpage at UIUC (USA).
- A ten-minute overview video [slide presentation](./overview.md).