# HG changeset patch
# User wenzelm
# Date 1226610396 -3600
# Node ID 9495aec512e2621944fb4a56a176673fc8035b97
# Parent  dd886b5756a77395d45bda57acf3b173c2f32245
renamed "Rules" to "Object-level rules";

diff -r dd886b5756a7 -r 9495aec512e2 doc-src/IsarImplementation/Thy/logic.thy
--- 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 {*