equal
deleted
inserted
replaced
176 |> simpset_of; |
176 |> simpset_of; |
177 |
177 |
178 fun hol_simplify ctxt rews = |
178 fun hol_simplify ctxt rews = |
179 Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews); |
179 Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews); |
180 |
180 |
181 fun unfold_tac ths ctxt = |
181 fun unfold_tac ctxt ths = |
182 ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths)); |
182 ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths)); |
183 |
183 |
184 end; |
184 end; |
185 |
185 |
186 structure Splitter = Simpdata.Splitter; |
186 structure Splitter = Simpdata.Splitter; |