equal
deleted
inserted
replaced
432 Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) |
432 Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) |
433 |
433 |
434 val avoids_parser = |
434 val avoids_parser = |
435 Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] |
435 Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] |
436 |
436 |
437 val main_parser = Parse.xname -- avoids_parser |
437 val main_parser = Parse.name -- avoids_parser |
438 in |
438 in |
439 val _ = |
439 val _ = |
440 Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} |
440 Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} |
441 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
441 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
442 (main_parser >> prove_strong_inductive_cmd) |
442 (main_parser >> prove_strong_inductive_cmd) |