src/HOL/Tools/inductive_package.ML
changeset 9643 c94db1a96f4e
parent 9625 77506775481e
child 9804 ee0c337327cf
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Aug 17 21:06:04 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 17 21:07:25 2000 +0200
     1.3 @@ -880,7 +880,7 @@
     1.4    OuterSyntax.improper_command "inductive_cases"
     1.5      "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
     1.6  
     1.7 -val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs", "of"];
     1.8 +val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
     1.9  val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
    1.10  
    1.11  end;