# HG changeset patch
# User wenzelm
# Date 1529583477 -7200
# Node ID 27be5b4cb80d10937156334999b8281d32b237b3
# Parent  f090b313fdc891ed592a7a99c8dea4f91abb4e25
more documentation;

diff -r f090b313fdc8 -r 27be5b4cb80d src/Doc/Eisbach/Preface.thy
--- 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