theorems [cases type: bool] = case_split;

--- a/src/HOL/PreList.thy	Wed Jun 14 17:47:18 2000 +0200
+++ b/src/HOL/PreList.thy	Wed Jun 14 17:59:53 2000 +0200
@@ -11,4 +11,6 @@
   Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
   SVC_Oracle:
 
+theorems [cases type: bool] = case_split
+
 end

--- a/src/HOL/Tools/induct_method.ML	Wed Jun 14 17:47:18 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Wed Jun 14 17:59:53 2000 +0200
@@ -191,6 +191,8 @@
   ...   cases ... R   - explicit rule
 *)
 
+val case_split = RuleCases.name ["True", "False"] case_split_thm;
+
 local
 
 fun cases_var thm =
@@ -217,7 +219,7 @@
 
     val rules =
       (case (args, facts) of
-        ((None, None), []) => [(case_split_thm, ["True", "False"])]
+        ((None, None), []) => [RuleCases.add case_split]
       | ((Some t, None), []) =>
           let val name = type_name t in
             (case lookup_casesT ctxt name of
@@ -427,6 +429,7 @@
      (inductN, induct_attr, "induction rule for type or set")],
    Method.add_methods
     [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
-     ("induct", induct_meth oo induct_args, "induction on types or sets")]];
+     ("induct", induct_meth oo induct_args, "induction on types or sets")],
+   (#1 o PureThy.add_thms [(("case_split", case_split), [])])];
 
 end;