doc-src/IsarRef/generic.tex
changeset 9936 f080397656d8
parent 9905 14a71104a498
child 9941 fe05af7ec816
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Sep 12 17:34:41 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Sep 12 17:34:50 2000 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4    folded & : & \isaratt \\[0.5ex]
     1.5    standard & : & \isaratt \\
     1.6    elimified & : & \isaratt \\
     1.7 -  no_vars & : & \isaratt \\
     1.8 +  no_vars^* & : & \isaratt \\
     1.9    exported^* & : & \isaratt \\
    1.10  \end{matharray}
    1.11  
    1.12 @@ -787,20 +787,23 @@
    1.13  
    1.14  \indexisarcmd{print-claset}
    1.15  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
    1.16 -\indexisaratt{iff}\indexisaratt{delrule}
    1.17 +\indexisaratt{iff}\indexisaratt{rule}
    1.18  \begin{matharray}{rcl}
    1.19    print_claset & : & \isarkeep{theory~|~proof} \\
    1.20    intro & : & \isaratt \\
    1.21    elim & : & \isaratt \\
    1.22    dest & : & \isaratt \\
    1.23 +  rule & : & \isaratt \\
    1.24    iff & : & \isaratt \\
    1.25 -  delrule & : & \isaratt \\
    1.26  \end{matharray}
    1.27  
    1.28  \begin{rail}
    1.29    ('intro' | 'elim' | 'dest') ('!' | () | '?')
    1.30    ;
    1.31 +  'rule' 'del'
    1.32 +  ;
    1.33    'iff' (() | 'add' | 'del')
    1.34 +  ;
    1.35  \end{rail}
    1.36  
    1.37  \begin{descr}
    1.38 @@ -813,13 +816,10 @@
    1.39    single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
    1.40    applied in the search-oriented automated methods, but only in single-step
    1.41    methods such as $rule$).
    1.42 -
    1.43 +\item [$rule~del$] deletes introduction, elimination, or destruct rules from
    1.44 +  the context.
    1.45  \item [$iff$] declares equations both as rules for the Simplifier and
    1.46    Classical Reasoner.
    1.47 -
    1.48 -\item [$delrule$] deletes introduction or elimination rules from the context.
    1.49 -  Note that destruction rules would have to be turned into elimination rules
    1.50 -  first, e.g.\ by using the $elimified$ attribute.
    1.51  \end{descr}
    1.52  
    1.53