equal
deleted
inserted
replaced
667 end; |
667 end; |
668 |
668 |
669 |
669 |
670 (* outer syntax *) |
670 (* outer syntax *) |
671 |
671 |
672 val _ = Keyword.keyword "avoids"; |
|
673 |
|
674 val _ = |
672 val _ = |
675 Outer_Syntax.local_theory_to_proof "nominal_inductive" |
673 Outer_Syntax.local_theory_to_proof "nominal_inductive" |
676 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" |
674 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" |
677 Keyword.thy_goal |
675 Keyword.thy_goal |
678 (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name -- |
676 (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name -- |