equal
deleted
inserted
replaced
132 |
132 |
133 (* atomize *) |
133 (* atomize *) |
134 |
134 |
135 fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule |
135 fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule |
136 (Drule.goals_conv (Library.equal i) |
136 (Drule.goals_conv (Library.equal i) |
137 (Drule.forall_conv |
137 (Drule.forall_conv ~1 |
138 (Drule.goals_conv (K true) (Tactic.rewrite true rews))))); |
138 (Drule.goals_conv (K true) (Tactic.rewrite true rews))))); |
139 |
139 |
140 fun atomize_term thy = |
140 fun atomize_term thy = |
141 drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; |
141 drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; |
142 |
142 |