changeset 69216 | 1a52baa70aed |
parent 68644 | 242d298526a3 |
child 69593 | 3dda49e08b9d |
--- a/src/HOL/Divides.thy Wed Oct 31 15:50:45 2018 +0100 +++ b/src/HOL/Divides.thy Wed Oct 31 15:53:32 2018 +0100 @@ -1278,7 +1278,7 @@ fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps) in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end - end; + end \<close>