equal
deleted
inserted
replaced
666 |
666 |
667 (* outer syntax *) |
667 (* outer syntax *) |
668 |
668 |
669 local structure P = OuterParse and K = OuterKeyword in |
669 local structure P = OuterParse and K = OuterKeyword in |
670 |
670 |
671 val _ = OuterSyntax.keywords ["avoids"]; |
671 val _ = OuterKeyword.keyword "avoids"; |
672 |
672 |
673 val _ = |
673 val _ = |
674 OuterSyntax.command "nominal_inductive" |
674 OuterSyntax.command "nominal_inductive" |
675 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal |
675 "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal |
676 (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name -- |
676 (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name -- |