src/HOL/Nominal/nominal_inductive.ML
changeset 24867 e5b55d7be9bb
parent 24861 cc669ca5f382
child 25824 f56dd9745d1b
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -511,22 +511,21 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val nominal_inductiveP =
     1.8 +val _ = OuterSyntax.keywords ["avoids"];
     1.9 +
    1.10 +val _ =
    1.11    OuterSyntax.command "nominal_inductive"
    1.12      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
    1.13      (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
    1.14        (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
    1.15          Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
    1.16  
    1.17 -val equivarianceP =
    1.18 +val _ =
    1.19    OuterSyntax.command "equivariance"
    1.20      "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
    1.21      (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
    1.22        (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
    1.23  
    1.24 -val _ = OuterSyntax.add_keywords ["avoids"];
    1.25 -val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];
    1.26 -
    1.27  end;
    1.28  
    1.29  end