| changeset 9804 | ee0c337327cf |
| parent 9643 | c94db1a96f4e |
| child 9831 | 9b883c416aef |
--- a/src/HOL/Tools/inductive_package.ML Sat Sep 02 21:49:51 2000 +0200 +++ b/src/HOL/Tools/inductive_package.ML Sat Sep 02 21:50:38 2000 +0200 @@ -877,7 +877,7 @@ >> (Toplevel.theory o inductive_cases); val inductive_casesP = - OuterSyntax.improper_command "inductive_cases" + OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules (improper)" K.thy_script ind_cases; val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];