equal
deleted
inserted
replaced
107 |> ProofContext.export ctxt' ctxt |
107 |> ProofContext.export ctxt' ctxt |
108 |> map (fn th => th RS mp) |
108 |> map (fn th => th RS mp) |
109 |> map zero_var_indexes |
109 |> map zero_var_indexes |
110 end |
110 end |
111 |
111 |
|
112 |
112 fun note_named_thm (name, thm) ctxt = |
113 fun note_named_thm (name, thm) ctxt = |
113 let |
114 let |
114 val thm_name = Binding.qualified_name |
115 val thm_name = Binding.qualified_name |
115 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
116 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
116 val attr = Attrib.internal (K eqvt_add) |
117 val attr = Attrib.internal (K eqvt_add) |
122 fun equivariance_cmd pred_name ctxt = |
123 fun equivariance_cmd pred_name ctxt = |
123 let |
124 let |
124 val thy = ProofContext.theory_of ctxt |
125 val thy = ProofContext.theory_of ctxt |
125 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
126 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
126 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
127 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
127 val thms = raw_equivariance preds raw_induct intrs ctxt |
128 val thms = raw_equivariance preds raw_induct intrs ctxt |
128 in |
129 in |
129 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
130 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
130 end |
131 end |
131 |
132 |
132 local structure P = Parse and K = Keyword in |
133 local structure P = Parse and K = Keyword in |