src/Doc/IsarRef/Generic.thy
changeset 55152 a56099a6447a
parent 55112 b1a5d603fd12
equal deleted inserted replaced
55151:f331472f1027 55152:a56099a6447a
   130     @{attribute_def unfolded} & : & @{text attribute} \\
   130     @{attribute_def unfolded} & : & @{text attribute} \\
   131     @{attribute_def folded} & : & @{text attribute} \\
   131     @{attribute_def folded} & : & @{text attribute} \\
   132     @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
   132     @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
   133     @{attribute_def rotated} & : & @{text attribute} \\
   133     @{attribute_def rotated} & : & @{text attribute} \\
   134     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
   134     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
   135     @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
       
   136     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   135     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   137   \end{matharray}
   136   \end{matharray}
   138 
   137 
   139   @{rail \<open>
   138   @{rail \<open>
   140     @@{attribute tagged} @{syntax name} @{syntax name}
   139     @@{attribute tagged} @{syntax name} @{syntax name}
   177   elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
   176   elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
   178   (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   177   (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   179   
   178   
   180   Note that the Classical Reasoner (\secref{sec:classical}) provides
   179   Note that the Classical Reasoner (\secref{sec:classical}) provides
   181   its own version of this operation.
   180   its own version of this operation.
   182 
       
   183   \item @{attribute standard} puts a theorem into the standard form of
       
   184   object-rules at the outermost theory level.  Note that this
       
   185   operation violates the local proof context (including active
       
   186   locales).
       
   187 
   181 
   188   \item @{attribute no_vars} replaces schematic variables by free
   182   \item @{attribute no_vars} replaces schematic variables by free
   189   ones; this is mainly for tuning output of pretty printed theorems.
   183   ones; this is mainly for tuning output of pretty printed theorems.
   190 
   184 
   191   \end{description}
   185   \end{description}