--- a/CookBook/Package/simple_inductive_package.ML Fri Feb 13 14:15:28 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Sat Feb 14 00:11:50 2009 +0000
@@ -6,6 +6,7 @@
(Binding.binding * typ) list -> (*{parameters}*)
((Binding.binding * Attrib.src list) * term) list -> (*{rules}*)
local_theory -> local_theory
+
val add_inductive:
(Binding.binding * string option * mixfix) list -> (*{predicates}*)
(Binding.binding * string option * mixfix) list -> (*{parameters}*)
@@ -170,7 +171,7 @@
end;
(* @end *)
-(* @chunk syntax *)
+(* @chunk parser *)
val parser =
OuterParse.opt_target --
OuterParse.fixes --
@@ -180,7 +181,9 @@
OuterParse.!!!
(OuterParse.enum1 "|"
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+(* @end *)
+(* @chunk syntax *)
val ind_decl =
parser >>
(fn (((loc, preds), params), specs) =>