src/HOL/Divides.thy
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>