'apply' consumes facts;
authorwenzelm
Thu May 18 11:40:57 2000 +0200 (2000-05-18)
changeset 88810467dd0d66ff
parent 8880 3a5215883047
child 8882 9df44a4f1bf7
'apply' consumes facts;
doc-src/IsarRef/pure.tex
src/Pure/Isar/isar_thy.ML
     1.1 --- a/doc-src/IsarRef/pure.tex	Wed May 17 18:27:13 2000 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Thu May 18 11:40:57 2000 +0200
     1.3 @@ -1017,9 +1017,10 @@
     1.4    order to complete the proof properly, any of the actual structured proof
     1.5    commands (e.g.\ ``$\DOT$'') has to be given eventually.
     1.6    
     1.7 -  Facts are passed to $m$ as indicated by the goal's forward-chain mode.
     1.8 -  Common use of $\isarkeyword{apply}$ would be in a purely backward manner,
     1.9 -  though.
    1.10 +  Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
    1.11 +  are \emph{consumed} afterwards.  Thus any further $\isarkeyword{apply}$
    1.12 +  command would always work in a purely backward manner.
    1.13 +
    1.14  \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
    1.15    terminal position.  Basically, this simulates a multi-step tactic script for
    1.16    $\QEDNAME$, but may be given anywhere within the proof body.
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Wed May 17 18:27:13 2000 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu May 18 11:40:57 2000 +0200
     2.3 @@ -379,9 +379,11 @@
     2.4  
     2.5  (* backward steps *)
     2.6  
     2.7 -fun apply (m, comment_ignore) = ProofHistory.applys (Method.refine m o Proof.assert_backward);
     2.8 -fun apply_end (m, comment_ignore) =
     2.9 -  ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
    2.10 +fun apply (m, comment_ignore) = ProofHistory.applys
    2.11 +  (Seq.map (Proof.goal_facts (K [])) o Method.refine m o Proof.assert_backward);
    2.12 +
    2.13 +fun apply_end (m, comment_ignore) = ProofHistory.applys
    2.14 +  (Method.refine_end m o Proof.assert_forward);
    2.15  
    2.16  val proof = ProofHistory.applys o Method.proof o
    2.17    apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;