src/HOL/Nominal/nominal_primrec.ML
changeset 21767 78ed5e22766a
parent 21618 1cbb1134cb6c
child 22101 6d13239d5f52
equal deleted inserted replaced
21766:3eb48154388e 21767:78ed5e22766a
   429   options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   429   options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   430 
   430 
   431 val primrecP =
   431 val primrecP =
   432   OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
   432   OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
   433     (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
   433     (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
   434       Toplevel.theory_to_proof
   434       Toplevel.print o Toplevel.theory_to_proof
   435         ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
   435         ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
   436           (map P.triple_swap eqns))));
   436           (map P.triple_swap eqns))));
   437 
   437 
   438 val _ = OuterSyntax.add_parsers [primrecP];
   438 val _ = OuterSyntax.add_parsers [primrecP];
   439 val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];
   439 val _ = OuterSyntax.add_keywords ["invariant", "freshness_context"];