theorems [cases type: bool] = case_split;
authorwenzelm
Wed Jun 14 17:59:53 2000 +0200 (2000-06-14)
changeset 9066b1e874e38dab
parent 9065 15f82c9aa331
child 9067 64464b5f6867
theorems [cases type: bool] = case_split;
src/HOL/PreList.thy
src/HOL/Tools/induct_method.ML
     1.1 --- a/src/HOL/PreList.thy	Wed Jun 14 17:47:18 2000 +0200
     1.2 +++ b/src/HOL/PreList.thy	Wed Jun 14 17:59:53 2000 +0200
     1.3 @@ -11,4 +11,6 @@
     1.4    Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
     1.5    SVC_Oracle:
     1.6  
     1.7 +theorems [cases type: bool] = case_split
     1.8 +
     1.9  end
     2.1 --- a/src/HOL/Tools/induct_method.ML	Wed Jun 14 17:47:18 2000 +0200
     2.2 +++ b/src/HOL/Tools/induct_method.ML	Wed Jun 14 17:59:53 2000 +0200
     2.3 @@ -191,6 +191,8 @@
     2.4    ...   cases ... R   - explicit rule
     2.5  *)
     2.6  
     2.7 +val case_split = RuleCases.name ["True", "False"] case_split_thm;
     2.8 +
     2.9  local
    2.10  
    2.11  fun cases_var thm =
    2.12 @@ -217,7 +219,7 @@
    2.13  
    2.14      val rules =
    2.15        (case (args, facts) of
    2.16 -        ((None, None), []) => [(case_split_thm, ["True", "False"])]
    2.17 +        ((None, None), []) => [RuleCases.add case_split]
    2.18        | ((Some t, None), []) =>
    2.19            let val name = type_name t in
    2.20              (case lookup_casesT ctxt name of
    2.21 @@ -427,6 +429,7 @@
    2.22       (inductN, induct_attr, "induction rule for type or set")],
    2.23     Method.add_methods
    2.24      [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
    2.25 -     ("induct", induct_meth oo induct_args, "induction on types or sets")]];
    2.26 +     ("induct", induct_meth oo induct_args, "induction on types or sets")],
    2.27 +   (#1 o PureThy.add_thms [(("case_split", case_split), [])])];
    2.28  
    2.29  end;