# HG changeset patch
# User wenzelm
# Date 966501453 -7200
# Node ID 77506775481e923fdd4c6ba776b113a589d60bb7
# Parent  de254f375477d823ecba4dac675f8baee85383f3
renamed 'mk_cases_tac' to 'ind_cases';

diff -r de254f375477 -r 77506775481e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Aug 17 10:37:04 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 17 10:37:33 2000 +0200
@@ -845,7 +845,7 @@
 
 val setup =
  [InductiveData.init,
-  Method.add_methods [("mk_cases_tac", mk_cases_meth oo mk_cases_args,
+  Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     "dynamic case analysis on sets")],
   Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
 
@@ -873,7 +873,7 @@
 
 
 val ind_cases =
-  P.opt_thm_name "=" -- Scan.repeat1 P.prop -- P.marg_comment
+  P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
   >> (Toplevel.theory o inductive_cases);
 
 val inductive_casesP =