src/ZF/Tools/induct_tacs.ML
changeset 24867 e5b55d7be9bb
parent 24826 78e6a3cea367
child 26336 a0e2b706ce73
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -188,6 +188,8 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
     1.8 +
     1.9  val rep_datatype_decl =
    1.10    (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
    1.11    (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
    1.12 @@ -195,13 +197,10 @@
    1.13    Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
    1.14    >> (fn (((x, y), z), w) => rep_datatype x y z w);
    1.15  
    1.16 -val rep_datatypeP =
    1.17 +val _ =
    1.18    OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
    1.19      (rep_datatype_decl >> Toplevel.theory);
    1.20  
    1.21 -val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
    1.22 -val _ = OuterSyntax.add_parsers [rep_datatypeP];
    1.23 -
    1.24  end;
    1.25  
    1.26  end;