equal
deleted
inserted
replaced
418 prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt |
418 prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt |
419 end |
419 end |
420 |
420 |
421 (* outer syntax *) |
421 (* outer syntax *) |
422 local |
422 local |
423 structure P = Parse; |
|
424 structure S = Scan |
|
425 |
|
426 val _ = Keyword.keyword "avoids" |
|
427 |
423 |
428 val single_avoid_parser = |
424 val single_avoid_parser = |
429 P.name -- (P.$$$ ":" |-- P.and_list1 P.term) |
425 Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) |
430 |
426 |
431 val avoids_parser = |
427 val avoids_parser = |
432 S.optional (P.$$$ "avoids" |-- P.enum1 "|" single_avoid_parser) [] |
428 Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] |
433 |
429 |
434 val main_parser = P.xname -- avoids_parser |
430 val main_parser = Parse.xname -- avoids_parser |
435 in |
431 in |
436 val _ = |
432 val _ = |
437 Outer_Syntax.local_theory_to_proof "nominal_inductive" |
433 Outer_Syntax.local_theory_to_proof ("nominal_inductive", Keyword.thy_goal) |
438 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
434 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
439 Keyword.thy_goal (main_parser >> prove_strong_inductive_cmd) |
435 (main_parser >> prove_strong_inductive_cmd) |
440 end |
436 end |
441 |
437 |
442 end |
438 end |