equal
deleted
inserted
replaced
428 Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] |
428 Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] |
429 |
429 |
430 val main_parser = Parse.xname -- avoids_parser |
430 val main_parser = Parse.xname -- avoids_parser |
431 in |
431 in |
432 val _ = |
432 val _ = |
433 Outer_Syntax.local_theory_to_proof ("nominal_inductive", Keyword.thy_goal) |
433 Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"} |
434 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
434 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
435 (main_parser >> prove_strong_inductive_cmd) |
435 (main_parser >> prove_strong_inductive_cmd) |
436 end |
436 end |
437 |
437 |
438 end |
438 end |