doc-src/IsarImplementation/Thy/logic.thy
changeset 28784 9495aec512e2
parent 28674 08a77c495dc1
child 28868 4fe0e90080ce
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Nov 13 22:05:49 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Nov 13 22:06:36 2008 +0100
@@ -309,8 +309,8 @@
   implicit in the de-Bruijn representation.  Names for bound variables
   in abstractions are maintained separately as (meaningless) comments,
   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is
-  commonplace in various standard operations (\secref{sec:rules}) that
-  are based on higher-order unification and matching.
+  commonplace in various standard operations (\secref{sec:obj-rules})
+  that are based on higher-order unification and matching.
 *}
 
 text %mlref {*
@@ -762,7 +762,7 @@
 *}
 
 
-section {* Rules \label{sec:rules} *}
+section {* Object-level rules \label{sec:obj-rules} *}
 
 text %FIXME {*