# HG changeset patch
# User wenzelm
# Date 1272058428 -7200
# Node ID 3567d0571932ec816fb97cacbc2fd7b9b9b1280d
# Parent  506d732cb52277f1a2298ea18bc6dcfca4d2ecef
eliminated spurious schematic statements;

diff -r 506d732cb522 -r 3567d0571932 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Apr 23 22:48:07 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Apr 23 23:33:48 2010 +0200
@@ -350,7 +350,7 @@
         (\<forall>x\<in>s. \<forall>j. j\<notin>{1..n} \<longrightarrow> (x j = p)) \<and>
         (\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x))"
 
-lemma ksimplexI:"card s = n + 1 \<Longrightarrow>  \<forall>x\<in>s. \<forall>j. x j \<le> p \<Longrightarrow> \<forall>x\<in>s. \<forall>j. j \<notin> {1..?n} \<longrightarrow> x j = ?p \<Longrightarrow> \<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x \<Longrightarrow> ksimplex p n s"
+lemma ksimplexI:"card s = n + 1 \<Longrightarrow>  \<forall>x\<in>s. \<forall>j. x j \<le> p \<Longrightarrow> \<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p \<Longrightarrow> \<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x \<Longrightarrow> ksimplex p n s"
   unfolding ksimplex_def by auto
 
 lemma ksimplex_eq: "ksimplex p n (s::(nat \<Rightarrow> nat) set) \<longleftrightarrow>
@@ -393,7 +393,7 @@
 
 lemma ksimplexD:
   assumes "ksimplex p n s"
-  shows "card s = n + 1" "finite s" "card s = n + 1" "\<forall>x\<in>s. \<forall>j. x j \<le> p" "\<forall>x\<in>s. \<forall>j. j \<notin> {1..?n} \<longrightarrow> x j = p"
+  shows "card s = n + 1" "finite s" "card s = n + 1" "\<forall>x\<in>s. \<forall>j. x j \<le> p" "\<forall>x\<in>s. \<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p"
   "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x" using assms unfolding ksimplex_eq by auto
 
 lemma ksimplex_successor:
diff -r 506d732cb522 -r 3567d0571932 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 23 22:48:07 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 23 23:33:48 2010 +0200
@@ -3327,7 +3327,7 @@
   using additive_tagged_division_1[OF _ assms(2), of "f o dest_vec1"]
   unfolding o_def vec1_dest_vec1 using assms(1) by auto
 
-lemma split_minus[simp]:"(\<lambda>(x, k). ?f x k) x - (\<lambda>(x, k). ?g x k) x = (\<lambda>(x, k). ?f x k - ?g x k) x"
+lemma split_minus[simp]:"(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
   unfolding split_def by(rule refl)
 
 lemma norm_triangle_le_sub: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"