--- a/src/HOL/Nominal/nominal_inductive.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Oct 06 16:50:04 2007 +0200
@@ -511,22 +511,21 @@
local structure P = OuterParse and K = OuterKeyword in
-val nominal_inductiveP =
+val _ = OuterSyntax.keywords ["avoids"];
+
+val _ =
OuterSyntax.command "nominal_inductive"
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
(P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
(P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
-val equivarianceP =
+val _ =
OuterSyntax.command "equivariance"
"prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
(P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
(fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
-val _ = OuterSyntax.add_keywords ["avoids"];
-val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];
-
end;
end