equal
deleted
inserted
replaced
454 ML {* |
454 ML {* |
455 |
455 |
456 fun prove_strong_ind (pred_name, avoids) ctxt = |
456 fun prove_strong_ind (pred_name, avoids) ctxt = |
457 Proof.theorem NONE (K I) [] ctxt |
457 Proof.theorem NONE (K I) [] ctxt |
458 |
458 |
459 local structure P = OuterParse and K = OuterKeyword in |
459 local structure P = Parse and K = Keyword in |
460 |
460 |
461 val _ = |
461 val _ = |
462 OuterSyntax.local_theory_to_proof "nominal_inductive" |
462 Outer_Syntax.local_theory_to_proof "nominal_inductive" |
463 "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal |
463 "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal |
464 (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- |
464 (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- |
465 (P.$$$ ":" |-- P.and_list1 P.term))) []) >> prove_strong_ind) |
465 (P.$$$ ":" |-- P.and_list1 P.term))) []) >> prove_strong_ind) |
466 |
466 |
467 end; |
467 end; |