changeset 25985 | 8d69087f6a4b |
parent 24893 | b8ef7afe3a6b |
child 26056 | 6a0801279f4c |
--- a/src/ZF/Tools/inductive_package.ML Sat Jan 26 17:08:43 2008 +0100 +++ b/src/ZF/Tools/inductive_package.ML Sat Jan 26 20:01:37 2008 +0100 @@ -584,7 +584,7 @@ val ind_decl = (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term -- - ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) -- + ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) -- (P.$$$ "intros" |-- P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) -- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --