apply: observe facts;
authorwenzelm
Sun Feb 13 20:58:13 2000 +0100 (2000-02-13 ago)
changeset 8236df3f983f5858
parent 8235 a4fb9be6b19a
child 8237 89002bc362c5
apply: observe facts;
apply_end;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Sun Feb 13 20:56:55 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Sun Feb 13 20:58:13 2000 +0100
     1.3 @@ -120,8 +120,8 @@
     1.4    val end_block: ProofHistory.T -> ProofHistory.T
     1.5    val defer: int option -> ProofHistory.T -> ProofHistory.T
     1.6    val prefer: int -> ProofHistory.T -> ProofHistory.T
     1.7 -  val tac: Method.text -> ProofHistory.T -> ProofHistory.T
     1.8 -  val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
     1.9 +  val apply: Method.text -> ProofHistory.T -> ProofHistory.T
    1.10 +  val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
    1.11    val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
    1.12      -> ProofHistory.T -> ProofHistory.T
    1.13    val qed: (Method.text * Comment.interest) option * Comment.text
    1.14 @@ -349,7 +349,7 @@
    1.15  
    1.16  (* shuffle state *)
    1.17  
    1.18 -fun shuffle meth i = Method.refine_no_facts (Method.Basic (K (meth i))) o Proof.assert_no_chain;
    1.19 +fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
    1.20  
    1.21  fun defer i = ProofHistory.applys (shuffle Method.defer i);
    1.22  fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
    1.23 @@ -357,8 +357,8 @@
    1.24  
    1.25  (* backward steps *)
    1.26  
    1.27 -fun tac m = ProofHistory.applys (Method.refine_no_facts m o Proof.assert_backward);
    1.28 -fun then_tac m = ProofHistory.applys (Method.refine m o Proof.assert_backward);
    1.29 +fun apply m = ProofHistory.applys (Method.refine m o Proof.assert_backward);
    1.30 +fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
    1.31  
    1.32  val proof = ProofHistory.applys o Method.proof o
    1.33    apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;