src/Pure/Isar/isar_thy.ML
changeset 8165 651b006d7eb8
parent 8090 5a241706d9b3
child 8204 b2a4a3d86b73
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jan 28 21:55:43 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jan 28 21:56:02 2000 +0100
     1.3 @@ -116,6 +116,8 @@
     1.4    val begin_block: ProofHistory.T -> ProofHistory.T
     1.5    val next_block: ProofHistory.T -> ProofHistory.T
     1.6    val end_block: ProofHistory.T -> ProofHistory.T
     1.7 +  val defer: int option -> ProofHistory.T -> ProofHistory.T
     1.8 +  val prefer: int -> ProofHistory.T -> ProofHistory.T
     1.9    val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.10    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.11    val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
    1.12 @@ -342,6 +344,12 @@
    1.13  val end_block = ProofHistory.applys Proof.end_block;
    1.14  
    1.15  
    1.16 +(* shuffle state *)
    1.17 +
    1.18 +fun defer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.defer i))));
    1.19 +fun prefer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.prefer i))));
    1.20 +
    1.21 +
    1.22  (* backward steps *)
    1.23  
    1.24  val tac = ProofHistory.applys o Method.refine_no_facts;