# HG changeset patch
# User wenzelm
# Date 1205789666 -3600
# Node ID e9a65675e5e8a9b4534b60851e7e61837c672367
# Parent  81a0fc28b0de5d0ac645ad09a54a65cad16ef3b6
avoid rebinding of existing facts;

diff -r 81a0fc28b0de -r e9a65675e5e8 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Mar 17 22:34:26 2008 +0100
@@ -56,7 +56,7 @@
 
 subsection {* Bounded Sequences *}
 
-lemma BseqI: assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
+lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
 unfolding Bseq_def
 proof (intro exI conjI allI)
   show "0 < max K 1" by simp
@@ -66,14 +66,11 @@
   thus "norm (X n) \<le> max K 1" by simp
 qed
 
-lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K"
-unfolding Bseq_def by simp
-
 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 unfolding Bseq_def by auto
 
-lemma BseqI2: assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
-proof (rule BseqI)
+lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
+proof (rule BseqI')
   let ?A = "norm ` X ` {..N}"
   have 1: "finite ?A" by simp
   have 2: "?A \<noteq> {}" by auto
@@ -96,7 +93,7 @@
 
 lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
 apply (erule BseqE)
-apply (rule_tac N="k" and K="K" in BseqI2)
+apply (rule_tac N="k" and K="K" in BseqI2')
 apply clarify
 apply (drule_tac x="n - k" in spec, simp)
 done
@@ -413,7 +410,7 @@
   obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
     using LIMSEQ_D [OF X r1] by fast
   show ?thesis
-  proof (rule BseqI2 [rule_format])
+  proof (rule BseqI2' [rule_format])
     fix n assume n: "N \<le> n"
     hence 1: "norm (X n - a) < r" by (rule N)
     hence 2: "X n \<noteq> 0" using r2 by auto
diff -r 81a0fc28b0de -r e9a65675e5e8 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Mar 17 22:34:26 2008 +0100
@@ -99,7 +99,7 @@
 by pat_completeness auto
 termination by lexicographic_order
 
-lemmas unionl_def = unionl.simps(2)
+lemmas unionl_eq = unionl.simps(2)
 
 function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
@@ -109,7 +109,7 @@
 by pat_completeness auto
 termination by lexicographic_order
 
-lemmas intersect_def = intersect.simps(3)
+lemmas intersect_eq = intersect.simps(3)
 
 function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
@@ -119,7 +119,7 @@
 by pat_completeness auto
 termination by lexicographic_order
 
-lemmas subtract_def = subtract.simps(3)
+lemmas subtract_eq = subtract.simps(3)
 
 function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 where
@@ -128,7 +128,7 @@
 by pat_completeness auto
 termination by lexicographic_order
 
-lemmas map_distinct_def = map_distinct.simps(2)
+lemmas map_distinct_eq = map_distinct.simps(2)
 
 function unions :: "'a list list \<Rightarrow> 'a list"
 where
@@ -137,7 +137,7 @@
 by pat_completeness auto
 termination by lexicographic_order
 
-lemmas unions_def = unions.simps(2)
+lemmas unions_eq = unions.simps(2)
 
 consts intersects :: "'a list list \<Rightarrow> 'a list"
 primrec
@@ -169,12 +169,12 @@
 
 lemma iso_union:
   "set (unionl xs ys) = set xs \<union> set ys"
-  unfolding unionl_def
+  unfolding unionl_eq
   by (induct xs arbitrary: ys) (simp_all add: iso_insert)
 
 lemma iso_intersect:
   "set (intersect xs ys) = set xs \<inter> set ys"
-  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
+  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
 
 definition
   subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -185,16 +185,16 @@
   assumes distnct: "distinct ys"
   shows "set (subtract' ys xs) = set ys - set xs"
     and "distinct (subtract' ys xs)"
-  unfolding subtract'_def flip_def subtract_def
+  unfolding subtract'_def flip_def subtract_eq
   using distnct by (induct xs arbitrary: ys) auto
 
 lemma iso_map_distinct:
   "set (map_distinct f xs) = image f (set xs)"
-  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
+  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
 
 lemma iso_unions:
   "set (unions xss) = \<Union> set (map set xss)"
-  unfolding unions_def
+  unfolding unions_eq
 proof (induct xss)
   case Nil show ?case by simp
 next
diff -r 81a0fc28b0de -r e9a65675e5e8 src/HOL/MetisExamples/BT.thy
--- a/src/HOL/MetisExamples/BT.thy	Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Mon Mar 17 22:34:26 2008 +0100
@@ -232,7 +232,7 @@
   done
 
 ML {*ResAtp.problem_name := "BT__bt_map_appnd"*}
-lemma bt_map_appnd:
+lemma (*bt_map_appnd:*)
      "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
   apply (induct t1)
   apply (metis appnd.simps(1) bt_map_appnd)
diff -r 81a0fc28b0de -r e9a65675e5e8 src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Mon Mar 17 22:34:26 2008 +0100
@@ -33,7 +33,7 @@
 
 declare [[reconstruction_modulus = 1]]
 
-lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
+lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
   apply auto
@@ -374,7 +374,7 @@
   apply (metis OrderedGroup.abs_le_D1 Orderings.linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.abs_mult)
   done
 
-lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
+lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
     f : O(g)" 
   apply (auto simp add: bigo_def)
 (*Version 2: single-step proof*)
diff -r 81a0fc28b0de -r e9a65675e5e8 src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/MetisExamples/set.thy	Mon Mar 17 22:34:26 2008 +0100
@@ -215,7 +215,7 @@
     "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
 by metis
 
-lemma fixedpoint:
+lemma (*fixedpoint:*)
     "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
 proof (neg_clausify)
 fix x xa