src/Pure/Isar/method.ML
changeset 8167 7574835ed01e
parent 8153 9bdbcb71dc56
child 8195 af2575a5c5ae
     1.1 --- a/src/Pure/Isar/method.ML	Fri Jan 28 21:56:37 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Jan 28 21:56:55 2000 +0100
     1.3 @@ -28,6 +28,8 @@
     1.4    val METHOD0: tactic -> Proof.method
     1.5    val fail: Proof.method
     1.6    val succeed: Proof.method
     1.7 +  val defer: int option -> Proof.method
     1.8 +  val prefer: int -> Proof.method
     1.9    val insert_tac: thm list -> int -> tactic
    1.10    val insert: thm list -> Proof.method
    1.11    val insert_facts: Proof.method
    1.12 @@ -195,6 +197,12 @@
    1.13  val succeed = METHOD (K all_tac);
    1.14  
    1.15  
    1.16 +(* shuffle *)
    1.17 +
    1.18 +fun prefer i = METHOD (K (PRIMITIVE (Thm.permute_prems 0 (i - 1))));
    1.19 +fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
    1.20 +
    1.21 +
    1.22  (* insert *)
    1.23  
    1.24  local