equal
deleted
inserted
replaced
182 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
182 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
183 in |
183 in |
184 equivariance preds raw_induct intrs ctxt |> snd |
184 equivariance preds raw_induct intrs ctxt |> snd |
185 end |
185 end |
186 |
186 |
187 local structure P = OuterParse and K = OuterKeyword in |
187 local structure P = Parse and K = Keyword in |
188 |
188 |
189 val _ = |
189 val _ = |
190 OuterSyntax.local_theory "equivariance" |
190 Outer_Syntax.local_theory "equivariance" |
191 "Proves equivariance for inductive predicate involving nominal datatypes." |
191 "Proves equivariance for inductive predicate involving nominal datatypes." |
192 K.thy_decl (P.xname >> equivariance_cmd); |
192 K.thy_decl (P.xname >> equivariance_cmd); |
193 end; |
193 end; |
194 |
194 |
195 end (* structure *) |
195 end (* structure *) |