renamed 'mk_cases_tac' to 'ind_cases';
authorwenzelm
Thu Aug 17 10:37:33 2000 +0200 (2000-08-17)
changeset 962577506775481e
parent 9624 de254f375477
child 9626 c4a45149cc46
renamed 'mk_cases_tac' to 'ind_cases';
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Aug 17 10:37:04 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 17 10:37:33 2000 +0200
     1.3 @@ -845,7 +845,7 @@
     1.4  
     1.5  val setup =
     1.6   [InductiveData.init,
     1.7 -  Method.add_methods [("mk_cases_tac", mk_cases_meth oo mk_cases_args,
     1.8 +  Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     1.9      "dynamic case analysis on sets")],
    1.10    Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
    1.11  
    1.12 @@ -873,7 +873,7 @@
    1.13  
    1.14  
    1.15  val ind_cases =
    1.16 -  P.opt_thm_name "=" -- Scan.repeat1 P.prop -- P.marg_comment
    1.17 +  P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
    1.18    >> (Toplevel.theory o inductive_cases);
    1.19  
    1.20  val inductive_casesP =