equal
deleted
inserted
replaced
187 |
187 |
188 local |
188 local |
189 |
189 |
190 fun unfold_prems n defs th = |
190 fun unfold_prems n defs th = |
191 if null defs then th |
191 if null defs then th |
192 else Conv.fconv_rule (Conv.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th; |
192 else Conv.fconv_rule (Conv.prems_conv n (K (MetaSimplifier.rewrite true defs))) th; |
193 |
193 |
194 fun unfold_prems_concls defs th = |
194 fun unfold_prems_concls defs th = |
195 if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th |
195 if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th |
196 else |
196 else |
197 Conv.fconv_rule |
197 Conv.fconv_rule |