--- 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.
*}
--- 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 {*