equal
deleted
inserted
replaced
483 end; |
483 end; |
484 |
484 |
485 |
485 |
486 (* outer syntax *) |
486 (* outer syntax *) |
487 |
487 |
488 local structure P = OuterParse and K = OuterKeyword in |
|
489 |
|
490 val _ = |
488 val _ = |
491 OuterSyntax.local_theory_to_proof "nominal_inductive2" |
489 Outer_Syntax.local_theory_to_proof "nominal_inductive2" |
492 "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal |
490 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
493 (P.xname -- |
491 Keyword.thy_goal |
494 Scan.option (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) -- |
492 (Parse.xname -- |
495 (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- |
493 Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) -- |
496 (P.$$$ ":" |-- P.and_list1 P.term))) []) >> (fn ((name, rule_name), avoids) => |
494 (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name -- |
|
495 (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) => |
497 prove_strong_ind name rule_name avoids)); |
496 prove_strong_ind name rule_name avoids)); |
498 |
497 |
499 end; |
|
500 |
|
501 end |
498 end |