renamed "delrule" to "rule del";
authorwenzelm
Tue Sep 12 17:34:50 2000 +0200 (2000-09-12)
changeset 9936f080397656d8
parent 9935 a87965201c34
child 9937 431c96ac997e
renamed "delrule" to "rule del";
doc-src/IsarRef/generic.tex
doc-src/IsarRef/pure.tex
     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  
     2.1 --- a/doc-src/IsarRef/pure.tex	Tue Sep 12 17:34:41 2000 +0200
     2.2 +++ b/doc-src/IsarRef/pure.tex	Tue Sep 12 17:34:50 2000 +0200
     2.3 @@ -845,7 +845,7 @@
     2.4  \ref{ch:hol-tools}).
     2.5  
     2.6  \indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
     2.7 -\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
     2.8 +\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
     2.9  \indexisaratt{OF}\indexisaratt{of}
    2.10  \begin{matharray}{rcl}
    2.11    assumption & : & \isarmeth \\
    2.12 @@ -857,7 +857,7 @@
    2.13    intro & : & \isaratt \\
    2.14    elim & : & \isaratt \\
    2.15    dest & : & \isaratt \\
    2.16 -  delrule & : & \isaratt \\
    2.17 +  rule & : & \isaratt \\
    2.18  \end{matharray}
    2.19  
    2.20  \begin{rail}
    2.21 @@ -867,6 +867,8 @@
    2.22    ;
    2.23    'of' insts ('concl' ':' insts)?
    2.24    ;
    2.25 +  'rule' 'del'
    2.26 +  ;
    2.27  \end{rail}
    2.28  
    2.29  \begin{descr}
    2.30 @@ -906,7 +908,7 @@
    2.31    attributes, and the $rule$ method, too.  In object-logics with classical
    2.32    reasoning enabled, the latter version should be used all the time to avoid
    2.33    confusion!
    2.34 -\item [$delrule$] undeclares introduction or elimination rules.
    2.35 +\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
    2.36  \end{descr}
    2.37  
    2.38