src/Pure/tactic.ML
changeset 16325 a6431098a929
parent 15977 aa6744dd998e
child 16425 2427be27cc60
     1.1 --- a/src/Pure/tactic.ML	Wed Jun 08 15:14:09 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Jun 08 16:11:09 2005 +0200
     1.3 @@ -111,10 +111,13 @@
     1.4    val simplify: bool -> thm list -> thm -> thm
     1.5    val conjunction_tac: tactic
     1.6    val smart_conjunction_tac: int -> tactic
     1.7 +  val prove_multi_plain: Sign.sg -> string list -> term list -> term list ->
     1.8 +    (thm list -> tactic) -> thm list
     1.9    val prove_multi: Sign.sg -> string list -> term list -> term list ->
    1.10      (thm list -> tactic) -> thm list
    1.11    val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
    1.12      (thm list -> tactic) -> thm list
    1.13 +  val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.14    val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.15    val prove_standard: Sign.sg -> string list -> term list -> term ->
    1.16      (thm list -> tactic) -> thm
    1.17 @@ -659,7 +662,7 @@
    1.18  
    1.19  (** minimal goal interface for programmed proofs *)
    1.20  
    1.21 -fun prove_multi sign xs asms props tac =
    1.22 +fun gen_prove_multi finish_thm sign xs asms props tac =
    1.23    let
    1.24      val prop = Logic.mk_conjunction_list props;
    1.25      val statement = Logic.list_implies (asms, prop);
    1.26 @@ -700,14 +703,19 @@
    1.27      |> map (fn res => res
    1.28        |> Drule.implies_intr_list casms
    1.29        |> Drule.forall_intr_list cparams
    1.30 -      |> norm_hhf_rule
    1.31 -      |> (#1 o Thm.varifyT' fixed_tfrees)
    1.32 -      |> Drule.zero_var_indexes)
    1.33 +      |> finish_thm fixed_tfrees)
    1.34    end;
    1.35  
    1.36 +fun prove_multi_plain sign xs asms prop tac =
    1.37 +  gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac;
    1.38 +fun prove_multi sign xs asms prop tac =
    1.39 +  gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
    1.40 +      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
    1.41 +    sign xs asms prop tac;
    1.42  fun prove_multi_standard sign xs asms prop tac =
    1.43    map Drule.standard (prove_multi sign xs asms prop tac);
    1.44  
    1.45 +fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac);
    1.46  fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
    1.47  fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);
    1.48