# HG changeset patch
# User wenzelm
# Date 1266782112 -3600
# Node ID 68dd8b51c6b81c271593e3670b5f679cbc147be1
# Parent  24c466b2cdc83f74ea856d0978c37d6aa84efef8
tuned headers;
tuned proofs;

diff -r 24c466b2cdc8 -r 68dd8b51c6b8 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Feb 21 20:54:40 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Feb 21 20:55:12 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Library/Euclidean_Space
+(*  Title:      Library/Multivariate_Analysis/Euclidean_Space.thy
     Author:     Amine Chaieb, University of Cambridge
 *)
 
@@ -66,8 +66,8 @@
 
 instantiation cart :: (plus,finite) plus
 begin
-definition  vector_add_def : "op + \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) + (y$i)))"
-instance ..
+  definition  vector_add_def : "op + \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) + (y$i)))"
+  instance ..
 end
 
 instantiation cart :: (times,finite) times
@@ -76,39 +76,42 @@
   instance ..
 end
 
-instantiation cart :: (minus,finite) minus begin
+instantiation cart :: (minus,finite) minus
+begin
   definition vector_minus_def : "op - \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) - (y$i)))"
-instance ..
+  instance ..
 end
 
-instantiation cart :: (uminus,finite) uminus begin
+instantiation cart :: (uminus,finite) uminus
+begin
   definition vector_uminus_def : "uminus \<equiv> (\<lambda> x.  (\<chi> i. - (x$i)))"
-instance ..
+  instance ..
 end
 
-instantiation cart :: (zero,finite) zero begin
+instantiation cart :: (zero,finite) zero
+begin
   definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"
-instance ..
+  instance ..
 end
 
-instantiation cart :: (one,finite) one begin
+instantiation cart :: (one,finite) one
+begin
   definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"
-instance ..
+  instance ..
 end
 
 instantiation cart :: (ord,finite) ord
- begin
-definition vector_le_def:
-  "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
-definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
-
-instance by (intro_classes)
+begin
+  definition vector_le_def:
+    "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
+  definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
+  instance by (intro_classes)
 end
 
 instantiation cart :: (scaleR, finite) scaleR
 begin
-definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x$i)))"
-instance ..
+  definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x$i)))"
+  instance ..
 end
 
 text{* Also the scalar-vector multiplication. *}
diff -r 24c466b2cdc8 -r 68dd8b51c6b8 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Feb 21 20:54:40 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Feb 21 20:55:12 2010 +0100
@@ -1,11 +1,11 @@
-(* Title:      HOL/Library/Finite_Cartesian_Product
-   Author:     Amine Chaieb, University of Cambridge
+(*  Title:      HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
+    Author:     Amine Chaieb, University of Cambridge
 *)
 
 header {* Definition of finite Cartesian product types. *}
 
 theory Finite_Cartesian_Product
-imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
+imports Main
 begin
 
 subsection {* Finite Cartesian products, with indexing and lambdas. *}
@@ -39,10 +39,7 @@
 *}
 
 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
-  apply auto
-  apply (rule ext)
-  apply auto
-  done
+  by (auto intro: ext)
 
 lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
   by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
@@ -75,7 +72,10 @@
   unfolding sndcart_def by simp
 
 lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
-by (auto, case_tac x, auto)
+  apply auto
+  apply (case_tac x)
+   apply auto
+  done
 
 lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x"
   by (simp add: Cart_eq)
@@ -90,9 +90,9 @@
   using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis
 
 lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"
-  by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
+  by (metis pastecart_fst_snd)
 
-lemma exists_pastecart: "(\<exists>p. P p)  \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
-  by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
+lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
+  by (metis pastecart_fst_snd)
 
 end