equal
deleted
inserted
replaced
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 |
127 |
128 val _ = |
128 val _ = |
129 Outer_Syntax.local_theory ("equivariance", Keyword.thy_decl) |
129 Outer_Syntax.local_theory @{command_spec "equivariance"} |
130 "Proves equivariance for inductive predicate involving nominal datatypes." |
130 "Proves equivariance for inductive predicate involving nominal datatypes." |
131 (Parse.xname >> equivariance_cmd) |
131 (Parse.xname >> equivariance_cmd) |
132 |
132 |
133 |
133 |
134 end (* structure *) |
134 end (* structure *) |