"inductive_cases": proper command;
authorwenzelm
Sat Sep 02 21:50:38 2000 +0200 (2000-09-02)
changeset 9804ee0c337327cf
parent 9803 bc883b390d91
child 9805 10b617bdd028
"inductive_cases": proper command;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Sep 02 21:49:51 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Sep 02 21:50:38 2000 +0200
     1.3 @@ -877,7 +877,7 @@
     1.4    >> (Toplevel.theory o inductive_cases);
     1.5  
     1.6  val inductive_casesP =
     1.7 -  OuterSyntax.improper_command "inductive_cases"
     1.8 +  OuterSyntax.command "inductive_cases"
     1.9      "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
    1.10  
    1.11  val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];