# HG changeset patch
# User wenzelm
# Date 1379936055 -7200
# Node ID 784223a8576ecaf1cf4282a1df0ce9362da9ffb4
# Parent  6a4e3299dfd17e6d5a428a066d4ddd1f48914258
proper text for document preparation;

diff -r 6a4e3299dfd1 -r 784223a8576e src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 23 12:40:34 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 23 13:34:15 2013 +0200
@@ -1438,10 +1438,10 @@
   qed (insert e, auto)
 qed
 
-text {* Hence the following eccentric variant of the inverse function theorem.    *)
-(* This has no continuity assumptions, but we do need the inverse function.  *)
-(* We could put f' \<circ> g = I but this happens to fit with the minimal linear   *)
-(* algebra theory I've set up so far. *}
+text {* Hence the following eccentric variant of the inverse function theorem.
+  This has no continuity assumptions, but we do need the inverse function.
+  We could put @{text "f' \<circ> g = I"} but this happens to fit with the minimal linear
+  algebra theory I've set up so far. *}
 
 (* move  before left_inverse_linear in Euclidean_Space*)