# 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 "\\\"}-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 {*