--- a/src/Doc/Eisbach/Preface.thy Thu Jun 21 12:39:52 2018 +0200
+++ b/src/Doc/Eisbach/Preface.thy Thu Jun 21 14:17:57 2018 +0200
@@ -31,6 +31,11 @@
necessarily Isabelle/ML. It covers the usage of the @{command method} as
well as the @{method match} method, as well as discussing their integration
with existing Isar concepts such as @{command named_theorems}.
+
+ These commands are provided by theory @{theory "Eisbach"} (see
+ \<^file>\<open>~~/src/HOL/Eisbach/Eisbach.thy\<close>): it needs to be imported by all Eisbach
+ applications. Theory theory @{theory "Eisbach_Tools"} provides additional
+ proof methods and attributes that are occasionally useful.
\<close>
end