1.1 --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Oct 10 20:49:25 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Mon Oct 11 21:05:01 2010 +0100
     1.3 @@ -31,8 +31,8 @@
     1.4  
     1.5    Many definitional packages for local theories are available in
     1.6    Isabelle.  Although a few old packages only work for global
     1.7 -  theories, the local theory interface is already the standard way of
     1.8 -  implementing definitional packages in Isabelle.
     1.9 +  theories, the standard way of implementing definitional packages in
    1.10 +  Isabelle is via the local theory interface.
    1.11  *}
    1.12  
    1.13  

     2.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 10 20:49:25 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 11 21:05:01 2010 +0100
     2.3 @@ -931,10 +931,17 @@
     2.4    constant @{text "c"}.  This technique of mapping names from one
     2.5    space into another requires some care in order to avoid conflicts.
     2.6    In particular, theorem names derived from a type constructor or type
     2.7 -  class are better suffixed in addition to the usual qualification,
     2.8 -  e.g.\ @{text "c_type.intro"} and @{text "c_class.intro"} for
     2.9 -  theorems related to type @{text "c"} and class @{text "c"},
    2.10 -  respectively.
    2.11 +  class should get an additional suffix in addition to the usual
    2.12 +  qualification.  This leads to the following conventions for derived
    2.13 +  names:
    2.14 +
    2.15 +  \medskip
    2.16 +  \begin{tabular}{ll}
    2.17 +  logical entity & fact name \\\hline
    2.18 +  constant @{text "c"} & @{text "c.intro"} \\
    2.19 +  type @{text "c"} & @{text "c_type.intro"} \\
    2.20 +  class @{text "c"} & @{text "c_class.intro"} \\
    2.21 +  \end{tabular}
    2.22  *}
    2.23  
    2.24  text %mlref {*