equal
deleted
inserted
replaced
122 val thms = raw_equivariance preds raw_induct intrs ctxt |
122 val thms = raw_equivariance preds raw_induct intrs ctxt |
123 in |
123 in |
124 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
124 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
125 end |
125 end |
126 |
126 |
127 local structure P = Parse and K = Keyword in |
|
128 |
127 |
129 val _ = |
128 val _ = |
130 Outer_Syntax.local_theory "equivariance" |
129 Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl) |
131 "Proves equivariance for inductive predicate involving nominal datatypes." |
130 "Proves equivariance for inductive predicate involving nominal datatypes." |
132 K.thy_decl (P.xname >> equivariance_cmd); |
131 (Parse.xname >> equivariance_cmd) |
133 |
132 |
134 end; |
|
135 |
133 |
136 end (* structure *) |
134 end (* structure *) |