# HG changeset patch
# User wenzelm
# Date 1286827501 -3600
# Node ID 08f59175e541323d08ad08487a0b9c5d2c7daf9d
# Parent  eb47307ab9301881de154032c24055aab6e9dd89
misc tuning;

diff -r eb47307ab930 -r 08f59175e541 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Oct 10 20:49:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Mon Oct 11 21:05:01 2010 +0100
@@ -31,8 +31,8 @@
 
   Many definitional packages for local theories are available in
   Isabelle.  Although a few old packages only work for global
-  theories, the local theory interface is already the standard way of
-  implementing definitional packages in Isabelle.
+  theories, the standard way of implementing definitional packages in
+  Isabelle is via the local theory interface.
 *}
 
 
diff -r eb47307ab930 -r 08f59175e541 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 10 20:49:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 11 21:05:01 2010 +0100
@@ -931,10 +931,17 @@
   constant @{text "c"}.  This technique of mapping names from one
   space into another requires some care in order to avoid conflicts.
   In particular, theorem names derived from a type constructor or type
-  class are better suffixed in addition to the usual qualification,
-  e.g.\ @{text "c_type.intro"} and @{text "c_class.intro"} for
-  theorems related to type @{text "c"} and class @{text "c"},
-  respectively.
+  class should get an additional suffix in addition to the usual
+  qualification.  This leads to the following conventions for derived
+  names:
+
+  \medskip
+  \begin{tabular}{ll}
+  logical entity & fact name \\\hline
+  constant @{text "c"} & @{text "c.intro"} \\
+  type @{text "c"} & @{text "c_type.intro"} \\
+  class @{text "c"} & @{text "c_class.intro"} \\
+  \end{tabular}
 *}
 
 text %mlref {*