Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use InductMethod.simp_case_tac;
authorwenzelm
Thu, 13 Jul 2000 11:42:11 +0200
changeset 9298 7d9b562a750b
parent 9297 bafe45732b10
child 9299 c5cda71de65d
use InductMethod.simp_case_tac;
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Thu Jul 13 11:41:40 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 13 11:42:11 2000 +0200
@@ -476,8 +476,8 @@
 fun mk_cases_i solved elims ss cprop =
   let
     val prem = Thm.assume cprop;
-    val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
-    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
+    val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
+    fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   in
     (case get_first (try mk_elim) elims of
       Some r => r
isabelle