1.1 --- a/doc-src/IsarRef/Thy/Framework.thy	Thu Feb 12 11:19:54 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Framework.thy	Thu Feb 12 11:36:15 2009 +0100
     1.3 @@ -886,10 +886,10 @@
     1.4    The present Isar infrastructure is sufficiently flexible to support
     1.5    calculational reasoning (chains of transitivity steps) as derived
     1.6    concept.  The generic proof elements introduced below depend on
     1.7 -  rules declared as @{text "[trans]"} in the context.  It is left to
     1.8 +  rules declared as @{attribute trans} in the context.  It is left to
     1.9    the object-logic to provide a suitable rule collection for mixed
    1.10 -  @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"}, @{text "\<subseteq>"} etc.
    1.11 -  Due to the flexibility of rule composition
    1.12 +  relations of @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"},
    1.13 +  @{text "\<subseteq>"} etc.  Due to the flexibility of rule composition
    1.14    (\secref{sec:framework-resolution}), substitution of equals by
    1.15    equals is covered as well, even substitution of inequalities
    1.16    involving monotonicity conditions; see also \cite[\S6]{Wenzel-PhD}
    1.17 @@ -902,10 +902,10 @@
    1.18    selected from the context.  The course of reasoning is organized by
    1.19    maintaining a secondary fact called ``@{fact calculation}'', apart
    1.20    from the primary ``@{fact this}'' already provided by the Isar
    1.21 -  primitives.  In the definitions below, @{attribute OF} is
    1.22 +  primitives.  In the definitions below, @{attribute OF} refers to
    1.23    @{inference resolution} (\secref{sec:framework-resolution}) with
    1.24 -  multiple rule arguments, and @{text "trans"} refers to a suitable
    1.25 -  rule from the context:
    1.26 +  multiple rule arguments, and @{text "trans"} represents to a
    1.27 +  suitable rule from the context:
    1.28  
    1.29    \begin{matharray}{rcl}
    1.30      @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\