doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 35613 9d3ff36ad4e1
parent 35351 7425aece4ee3
child 35744 93603d7b8ee9
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 06 15:34:29 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 06 15:39:16 2010 +0100
     1.3 @@ -795,16 +795,15 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    'iprover' ('!' ?) ( rulemod * )
     1.8 +    'iprover' ( rulemod * )
     1.9      ;
    1.10    \end{rail}
    1.11  
    1.12    The @{method (HOL) iprover} method performs intuitionistic proof
    1.13    search, depending on specifically declared rules from the context,
    1.14    or given as explicit arguments.  Chained facts are inserted into the
    1.15 -  goal before commencing proof search; ``@{method (HOL) iprover}@{text
    1.16 -  "!"}''  means to include the current @{fact prems} as well.
    1.17 -  
    1.18 +  goal before commencing proof search.
    1.19 +
    1.20    Rules need to be classified as @{attribute (Pure) intro},
    1.21    @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
    1.22    ``@{text "!"}'' indicator refers to ``safe'' rules, which may be