summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 23 Sep 2013 13:34:15 +0200 | |

changeset 53799 | 784223a8576e |

parent 53798 | 6a4e3299dfd1 |

child 53800 | ac1ec5065316 |

proper text for document preparation;

--- 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*)