Goal.prove: more tactic arguments;
authorwenzelm
Sat Jul 29 00:51:29 2006 +0200 (2006-07-29 ago)
changeset 202487916ce5bb069
parent 20247 32fb8d2715de
child 20249 a13adb4f94dc
Goal.prove: more tactic arguments;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 28 18:37:25 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Jul 29 00:51:29 2006 +0200
     1.3 @@ -507,7 +507,7 @@
     1.4    in
     1.5      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
     1.6        SkipProof.prove ctxt [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     1.7 -        (fn prems => EVERY
     1.8 +        (fn {prems, ...} => EVERY
     1.9            [cut_facts_tac [hd prems] 1,
    1.10             rewrite_goals_tac rec_sets_defs,
    1.11             dtac (unfold RS subst) 1,
    1.12 @@ -653,7 +653,7 @@
    1.13              else ();
    1.14  
    1.15      val induct = standard (SkipProof.prove ctxt [] ind_prems ind_concl
    1.16 -      (fn prems => EVERY
    1.17 +      (fn {prems, ...} => EVERY
    1.18          [rewrite_goals_tac [inductive_conj_def],
    1.19           rtac (impI RS allI) 1,
    1.20           DETERM (etac raw_fp_induct 1),
     2.1 --- a/src/HOL/Tools/record_package.ML	Fri Jul 28 18:37:25 2006 +0200
     2.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jul 29 00:51:29 2006 +0200
     2.3 @@ -1438,7 +1438,7 @@
     2.4  
     2.5      fun induct_prf () =
     2.6        let val (assm, concl) = induct_prop
     2.7 -      in prove_standard [assm] concl (fn prems =>
     2.8 +      in prove_standard [assm] concl (fn {prems, ...} =>
     2.9             EVERY [try_param_tac rN abs_induct 1,
    2.10                    simp_tac (HOL_ss addsimps [split_paired_all]) 1,
    2.11                    resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
    2.12 @@ -1878,7 +1878,7 @@
    2.13      fun induct_prf () =
    2.14        let val (assm, concl) = induct_prop;
    2.15        in
    2.16 -        prove_standard [assm] concl (fn prems =>
    2.17 +        prove_standard [assm] concl (fn {prems, ...} =>
    2.18            try_param_tac rN induct_scheme 1
    2.19            THEN try_param_tac "more" unit_induct 1
    2.20            THEN resolve_tac prems 1)
     3.1 --- a/src/Pure/Isar/skip_proof.ML	Fri Jul 28 18:37:25 2006 +0200
     3.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Jul 29 00:51:29 2006 +0200
     3.3 @@ -9,8 +9,8 @@
     3.4  sig
     3.5    val make_thm: theory -> term -> thm
     3.6    val cheat_tac: theory -> tactic
     3.7 -  val prove: ProofContext.context ->
     3.8 -    string list -> term list -> term -> (thm list -> tactic) -> thm
     3.9 +  val prove: ProofContext.context -> string list -> term list -> term ->
    3.10 +    ({prems: thm list, context: Context.proof} -> tactic) -> thm
    3.11  end;
    3.12  
    3.13  structure SkipProof: SKIP_PROOF =