1.1 --- a/src/HOL/HOL.thy	Tue Jun 10 19:15:18 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 10 19:15:19 2008 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    "~~/src/Tools/random_word.ML"
     1.5    "~~/src/Tools/atomize_elim.ML"
     1.6    "~~/src/Tools/induct.ML"
     1.7 +  ("~~/src/HOL/Tools/induct_tacs.ML")
     1.8    "~~/src/Tools/code/code_name.ML"
     1.9    "~~/src/Tools/code/code_funcgr.ML"
    1.10    "~~/src/Tools/code/code_thingol.ML"
    1.11 @@ -721,7 +722,7 @@
    1.12    case distinction as a natural deduction rule.
    1.13    Note that @{term "~P"} is the second case, not the first
    1.14  *}
    1.15 -lemma case_split_thm:
    1.16 +lemma case_split [case_names True False]:
    1.17    assumes prem1: "P ==> Q"
    1.18        and prem2: "~P ==> Q"
    1.19    shows "Q"
    1.20 @@ -729,7 +730,10 @@
    1.21  apply (erule prem2)
    1.22  apply (erule prem1)
    1.23  done
    1.24 -lemmas case_split = case_split_thm [case_names True False]
    1.25 +
    1.26 +ML {*
    1.27 +  fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split}
    1.28 +*}
    1.29  
    1.30  (*Classical implies (-->) elimination. *)
    1.31  lemma impCE:
    1.32 @@ -1487,9 +1491,9 @@
    1.33  ML {*
    1.34  structure ProjectRule = ProjectRuleFun
    1.35  (
    1.36 -  val conjunct1 = @{thm conjunct1};
    1.37 -  val conjunct2 = @{thm conjunct2};
    1.38 -  val mp = @{thm mp};
    1.39 +  val conjunct1 = @{thm conjunct1}
    1.40 +  val conjunct2 = @{thm conjunct2}
    1.41 +  val mp = @{thm mp}
    1.42  )
    1.43  *}
    1.44  
    1.45 @@ -1543,17 +1547,20 @@
    1.46  text {* Method setup. *}
    1.47  
    1.48  ML {*
    1.49 -  structure Induct = InductFun
    1.50 -  (
    1.51 -    val cases_default = @{thm case_split}
    1.52 -    val atomize = @{thms induct_atomize}
    1.53 -    val rulify = @{thms induct_rulify}
    1.54 -    val rulify_fallback = @{thms induct_rulify_fallback}
    1.55 -  );
    1.56 +structure Induct = InductFun
    1.57 +(
    1.58 +  val cases_default = @{thm case_split}
    1.59 +  val atomize = @{thms induct_atomize}
    1.60 +  val rulify = @{thms induct_rulify}
    1.61 +  val rulify_fallback = @{thms induct_rulify_fallback}
    1.62 +)
    1.63  *}
    1.64  
    1.65  setup Induct.setup
    1.66  
    1.67 +use "~~/src/HOL/Tools/induct_tacs.ML"
    1.68 +setup InductTacs.setup
    1.69 +
    1.70  
    1.71  subsection {* Other simple lemmas and lemma duplicates *}
    1.72  
    1.73 @@ -1578,7 +1585,7 @@
    1.74    apply (erule_tac x = "%z. if z = x then y else f z" in allE)
    1.75    apply (erule impE)
    1.76    apply (rule allI)
    1.77 -  apply (rule_tac P = "xa = x" in case_split_thm)
    1.78 +  apply (case_tac "xa = x")
    1.79    apply (drule_tac [3] x = x in fun_cong, simp_all)
    1.80    done
    1.81  
    1.82 @@ -1735,7 +1742,6 @@
    1.83  val all_simps = thms "all_simps";
    1.84  val atomize_not = thm "atomize_not";
    1.85  val case_split = thm "case_split";
    1.86 -val case_split_thm = thm "case_split_thm"
    1.87  val cases_simp = thm "cases_simp";
    1.88  val choice_eq = thm "choice_eq"
    1.89  val cong = thm "cong"