--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Aug 23 07:12:05 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Aug 23 14:11:02 2011 -0700
@@ -180,7 +180,7 @@
"(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
"(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
"(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
- unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv
+ unfolding interval_bij_cart vector_component_simps o_def split_conv
unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
from z(1) guess zf unfolding image_iff .. note zf=this
from z(2) guess zg unfolding image_iff .. note zg=this