src/HOL/Deriv.thy
changeset 69216 1a52baa70aed
parent 69111 a3efc22181a8
child 69593 3dda49e08b9d
--- a/src/HOL/Deriv.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Deriv.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -62,7 +62,7 @@
         fn context =>
           Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros}
           |> map_filter eq_rule)
-  end;
+  end
 \<close>
 
 text \<open>