# HG changeset patch
# User wenzelm
# Date 1030438985 -7200
# Node ID 604d0f3622d63ee4306899c335d02c5ea8c3b786
# Parent  079af5c90d1cefe5d447dfaa49341d62ff59cae4
*** empty log message ***

diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -766,15 +766,6 @@
 apply   (auto intro: MGFNormalI)
 done
 
-lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
-apply (rule MGF_asm)
-apply (intro strip)
-apply (rule MGFNormalI)
-apply (rule ax_derivs.weaken)
-apply  (erule MGF_simult_Methd)
-apply auto
-done
-
 
 section "corollaries"
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -567,11 +567,6 @@
                             fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
                           | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
 
-lemma method_declared_inI:
-  "\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk> 
-   \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
-by (auto simp add: declared_in_def cdeclaredmethd_def)
-
 
 subsubsection "members"
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -126,7 +126,7 @@
 lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
-lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn"
+lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
 section "classes and interfaces"
@@ -687,10 +687,6 @@
   "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
 by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
 
-lemma Base_foo_member_of_Base: 
-  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
-by (auto intro!: members.Immediate Base_declares_foo)
-
 lemma Ext_foo_member_of_Ext: 
   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
 by (auto intro!: members.Immediate Ext_declares_foo)
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/State.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -577,7 +577,7 @@
 apply auto
 done
 
-lemma raise_if_SomeD [dest!]:
+lemma error_if_SomeD [dest!]:
   "error_if c e y = Some z \<Longrightarrow> c \<and> z=(Error e) \<and> y=None \<or> (y=Some z)"
 apply (case_tac y)
 apply (case_tac c)
@@ -773,7 +773,7 @@
  "\<not> (\<exists> err. x=Error err) \<Longrightarrow> error_free ((Some x),s)"
 by (auto simp add: error_free_def)
 
-lemma error_free_absorb [simp,intro]: 
+lemma error_free_abupd_absorb [simp,intro]: 
  "error_free s \<Longrightarrow> error_free (abupd (absorb j) s)"
 by (cases s) 
    (auto simp add: error_free_def absorb_def
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/WellType.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -518,14 +518,15 @@
 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
 by (auto simp add: is_acc_iface_def)
 
-lemma is_acc_iface_is_accessible: 
+lemma is_acc_iface_Iface_is_accessible: 
   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
 by (auto simp add: is_acc_iface_def)
 
 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
 by (auto simp add: is_acc_type_def)
 
-lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
+lemma is_acc_iface_is_accessible:
+  "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
 by (auto simp add: is_acc_type_def)
 
 lemma wt_Methd_is_methd: 
@@ -539,13 +540,6 @@
  * conclusion (no selectors in the conclusion\<dots>)
  *)
 
-lemma wt_Super:
-"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
-  class (prg E) C = Some c;D=super c\<rbrakk> 
- \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
-by (auto elim: wt.Super)
- 
-
 lemma wt_Call: 
 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -764,15 +764,6 @@
 apply simp
 done
 
-lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
-apply(subgoal_tac "length xs<length (x # xs)")
- apply(drule_tac Q=Q in  lift_nth)
- apply(erule ssubst)
- apply (simp add:lift_def)
- apply(case_tac "(x # xs) ! length xs",simp)
-apply simp
-done
-
 lemma Seq_sound: 
   "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
   \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
@@ -915,37 +906,6 @@
 
 subsubsection{* Soundness of the While rule *}
 
-lemma assum_after_body: 
-  "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
-  (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None; 
-   s \<in> b;  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
-            map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
-  \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys 
-      \<in> assum (pre, rely)"
-apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
-apply clarify
-apply(erule_tac x=s in allE)
-apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
- apply clarify
- apply(erule_tac x="Suc i" in allE)
- apply simp
- apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
- apply(erule mp)
- apply(erule etran.elims,simp)
- apply(case_tac "fst(((Some P, s) # xs) ! i)")
-  apply(force intro:Env simp add:lift_def)
- apply(force intro:Env simp add:lift_def)
-apply(rule conjI)
- apply(simp add:comm_def last_length)
-apply clarify
-apply(erule_tac x="Suc(length xs + i)" in allE,simp)
-apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps)
- apply(erule mp)
- apply(case_tac "((Some P, s) # xs) ! length xs")
- apply(simp add:lift_def)
-apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
-done
-
 lemma last_append[rule_format]:
   "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
 apply(induct ys)
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Hyperreal/EvenOdd.ML
--- a/src/HOL/Hyperreal/EvenOdd.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -204,8 +204,8 @@
 Goal "0 < n & even n --> 1 < n";
 by (induct_tac "n" 1);
 by Auto_tac;
-qed_spec_mp "even_gt_zero_gt_one";
-bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one);
+qed_spec_mp "even_gt_zero_gt_one_aux";
+bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux);
 
 (* more general *)
 Goal "n div 2 <= (Suc n) div 2";
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/IMP/Transition.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -604,7 +604,7 @@
   ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
 qed
 
-lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
+lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
 apply (erule evalc.induct)
 
 -- SKIP 
@@ -680,7 +680,7 @@
   apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   done
 
-lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   apply (fastsimp dest: FB_lemma2)
   done
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/IMPP/Hoare.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -352,10 +352,10 @@
 by (Simp_tac 1);
 by (eatac MGF_lemma2_simult 1 1);
 by (rtac subset_refl 1);
-qed "MGF";
+qed "MGF'";
 
 (* requires Body+empty+insert / BodyN, com_det *)
-bind_thm ("hoare_complete", MGF RS MGF_complete); 
+bind_thm ("hoare_complete", MGF' RS MGF_complete); 
 
 section "unused derived rules";
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Induct/LList.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -502,7 +502,7 @@
 apply (auto simp add: Rep_LList_inject)
 done
 
-lemma LList_fun_equalityI: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
+lemma CONS_D2: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
 apply (erule llist.cases)
 apply (erule CONS_neq_NIL, fast)
 done
@@ -613,7 +613,7 @@
 done
 
 text{*strong co-induction: bisimulation and case analysis on one variable*}
-lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
+lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
 apply (rule_tac X = " (%u. Lappend u N) `llist (A) " in llist_coinduct)
 apply (erule imageI)
 apply (rule image_subsetI)
@@ -893,14 +893,14 @@
 done
 
 text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*}
-lemma lmap_lappend_distrib:
+lemma lmap_lappend_distrib':
      "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
 apply (rule_tac l = "l" in llist_fun_equalityI, simp)
 apply simp
 done
 
 text{*Without strong coinduction, three case analyses might be needed*}
-lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
+lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
 apply (rule_tac l = "l1" in llist_fun_equalityI, simp)
 apply simp
 done
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -352,12 +352,12 @@
 
 (*** division of a number by itself ***)
 
-lemma lemma1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
+lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
 apply (subgoal_tac "0 < a*q")
  apply (simp add: int_0_less_mult_iff, arith)
 done
 
-lemma lemma2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
+lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
 apply (subgoal_tac "0 <= a* (1-q) ")
  apply (simp add: int_0_le_mult_iff)
 apply (simp add: zdiff_zmult_distrib2)
@@ -366,9 +366,9 @@
 lemma self_quotient: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> q = 1"
 apply (simp add: split_ifs quorem_def linorder_neq_iff)
 apply (rule order_antisym, auto)
-apply (rule_tac [3] a = "-a" and r = "-r" in lemma1)
-apply (rule_tac a = "-a" and r = "-r" in lemma2)
-apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+
+apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
+apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
+apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+
 done
 
 lemma self_remainder: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> r = 0"
@@ -699,7 +699,7 @@
 
 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
 
-lemma lemma1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
+lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
 apply (subgoal_tac "b * (c - q mod c) < r * 1")
 apply (simp add: zdiff_zmult_distrib2)
 apply (rule order_le_less_trans)
@@ -709,19 +709,19 @@
                       add1_zle_eq pos_mod_bound)
 done
 
-lemma lemma2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
+lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
 apply (subgoal_tac "b * (q mod c) <= 0")
  apply arith
 apply (simp add: zmult_le_0_iff pos_mod_sign)
 done
 
-lemma lemma3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
+lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
 apply (subgoal_tac "0 <= b * (q mod c) ")
 apply arith
 apply (simp add: int_0_le_mult_iff pos_mod_sign)
 done
 
-lemma lemma4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
+lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
 apply (simp add: zdiff_zmult_distrib2)
 apply (rule order_less_le_trans)
@@ -735,7 +735,7 @@
       ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
 by (auto simp add: zmult_ac quorem_def linorder_neq_iff
                    int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
-                   lemma1 lemma2 lemma3 lemma4)
+                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
 
 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
 apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
@@ -751,17 +751,17 @@
 
 (*** Cancellation of common factors in div ***)
 
-lemma lemma1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
+lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
 by (subst zdiv_zmult2_eq, auto)
 
-lemma lemma2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
+lemma zdiv_zmult_zmult1_aux2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
 apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
-apply (rule_tac [2] lemma1, auto)
+apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
 done
 
 lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
 apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
-apply (auto simp add: linorder_neq_iff lemma1 lemma2)
+apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
 done
 
 lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b"
@@ -773,18 +773,18 @@
 
 (*** Distribution of factors over mod ***)
 
-lemma lemma1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
+lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
 by (subst zmod_zmult2_eq, auto)
 
-lemma lemma2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
+lemma zmod_zmult_zmult1_aux2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
 apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
-apply (rule_tac [2] lemma1, auto)
+apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
 done
 
 lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
 apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
 apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
-apply (auto simp add: linorder_neq_iff lemma1 lemma2)
+apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
 done
 
 lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -148,7 +148,7 @@
  better idea of what is actually going on.
 *}
 
-lemma exec_append:
+lemma exec_append':
   "ALL stack. exec (xs @ ys) stack env
     = exec ys (exec xs stack env) env" (is "?P xs")
 proof (induct xs)
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -643,7 +643,7 @@
 apply (auto intro: rtrancl_trans)
 done
 
-lemmas defs1 = defs1 raise_system_xcpt_def
+lemmas defs2 = defs1 raise_system_xcpt_def
 
 lemma Checkcast_correct:
 "\<lbrakk> wt_jvm_prog G phi;
@@ -654,7 +654,7 @@
     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
     fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
+apply (clarsimp simp add: defs2 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
 apply (blast intro: Cast_conf2)
 done
 
@@ -668,12 +668,12 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def 
+apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def 
                 split: option.split split_if_asm)
 apply (frule conf_widen)
 apply assumption+
 apply (drule conf_RefTD)
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
 apply (rule conjI)
  apply (drule widen_cfs_fields)
  apply assumption+
@@ -700,7 +700,7 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
 apply (frule conf_widen)
 prefer 2
   apply assumption
@@ -1110,7 +1110,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
 apply fast
 done
 
@@ -1123,7 +1123,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
 apply fast
 done
 
@@ -1135,7 +1135,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
 apply fast
 done
 
@@ -1147,7 +1147,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
@@ -1159,7 +1159,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
@@ -1171,7 +1171,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
@@ -1183,7 +1183,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
@@ -1195,7 +1195,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
+apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def conf_def)
 apply blast
 done
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NanoJava/State.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -121,7 +121,7 @@
   "get_field (set_locs l s) a f = get_field s a f"
 by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
 
-lemma get_field_set_locs [simp]:
+lemma get_field_del_locs [simp]:
   "get_field (del_locs s) a f = get_field s a f"
 by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/NumberTheory/BijectionRel.thy
--- a/src/HOL/NumberTheory/BijectionRel.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -77,26 +77,27 @@
     done
 qed
 
-lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
+lemma inj_func_bijR_aux1:
+    "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
   apply (unfold inj_on_def)
   apply auto
   done
 
-lemma aux:
+lemma inj_func_bijR_aux2:
   "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
     ==> (F, f ` F) \<in> bijR P"
   apply (rule_tac F = F and A = A in aux_induct)
      apply (rule finite_subset)
       apply auto
   apply (rule bijR.insert)
-     apply (rule_tac [3] aux)
+     apply (rule_tac [3] inj_func_bijR_aux1)
         apply auto
   done
 
 lemma inj_func_bijR:
   "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
     ==> (A, f ` A) \<in> bijR P"
-  apply (rule aux)
+  apply (rule inj_func_bijR_aux2)
      apply auto
   done
 
@@ -166,14 +167,14 @@
       apply auto
   done
 
-lemma aux: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
+lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
   apply auto
   done
 
 lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)"
   apply (unfold bijP_def)
   apply (rule iffI)
-  apply (erule_tac [!] aux)
+  apply (erule_tac [!] aux_foo)
       apply simp_all
   apply (rule iffD2)
    apply (rule_tac P = P in aux_sym)
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -139,7 +139,7 @@
 
 subsection {* Chinese: uniqueness *}
 
-lemma aux:
+lemma zcong_funprod_aux:
   "m_cond n mf ==> km_cond n kf mf
     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
     ==> [x = y] (mod mf n)"
@@ -160,10 +160,10 @@
     [x = y] (mod funprod mf 0 n)"
   apply (induct n)
    apply (simp_all (no_asm))
-   apply (blast intro: aux)
+   apply (blast intro: zcong_funprod_aux)
   apply (rule impI)+
   apply (rule zcong_zgcd_zmult_zmod)
-    apply (blast intro: aux)
+    apply (blast intro: zcong_funprod_aux)
     prefer 2
     apply (subst zgcd_commute)
     apply (rule funprod_zgcd)
@@ -192,7 +192,7 @@
     apply simp_all
   done
 
-lemma aux:
+lemma x_sol_lin_aux:
     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
   apply (unfold mhf_def)
   apply (case_tac "i = 0")
@@ -215,7 +215,7 @@
      apply auto
   apply (subst zdvd_iff_zmod_eq_0 [symmetric])
   apply (rule zdvd_zmult)
-  apply (rule aux)
+  apply (rule x_sol_lin_aux)
   apply auto
   done
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -142,7 +142,7 @@
    apply auto
   done
 
-lemma aux: "a \<le> b - 1 ==> a < (b::int)"
+lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
   apply auto
   done
 
@@ -154,7 +154,7 @@
    apply auto
    apply (rule_tac [2] m = m in zcong_zless_imp_eq)
        apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
-	 order_less_imp_le aux simp add: zcong_sym)
+	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
   apply (rule_tac "x" = "b" in exI)
   apply safe
   apply (rule Bnor_mem_if)
@@ -280,7 +280,7 @@
   done
 
 
-lemma aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
+lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   apply (unfold inj_on_def)
   apply auto
   done
@@ -295,7 +295,7 @@
    apply auto
   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   apply (subst setprod_insert)
-    apply (rule_tac [2] aux)
+    apply (rule_tac [2] Bnor_prod_power_aux)
      apply (unfold inj_on_def)
      apply (simp_all add: zmult_ac Bnor_fin finite_imageI
        Bnor_mem_zle_swap)
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -343,7 +343,7 @@
    apply simp_all
   done
 
-lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
+lemma zrelprime_zdvd_zmult_aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
   apply (subgoal_tac "m = zgcd (m * n, m * k)")
    apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
    apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
@@ -351,9 +351,9 @@
 
 lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
   apply (case_tac "0 \<le> m")
-   apply (blast intro: aux)
+   apply (blast intro: zrelprime_zdvd_zmult_aux)
   apply (subgoal_tac "k dvd -m")
-   apply (rule_tac [2] aux)
+   apply (rule_tac [2] zrelprime_zdvd_zmult_aux)
      apply auto
   done
 
@@ -618,18 +618,13 @@
   apply (auto simp add: zcong_iff_lin)
   done
 
-lemma aux: "a = c ==> b = d ==> a - b = c - (d::int)"
-  apply auto
-  done
-
-lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
+lemma zcong_zmod_aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
 by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
 
-
 lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   apply (unfold zcong_def)
   apply (rule_tac t = "a - b" in ssubst)
-  apply (rule_tac "m" = "m" in aux)
+  apply (rule_tac "m" = "m" in zcong_zmod_aux)
   apply (rule trans)
    apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
   apply (simp add: zadd_commute)
@@ -643,7 +638,7 @@
        apply (simp_all add: pos_mod_bound pos_mod_sign)
   apply (unfold zcong_def dvd_def)
   apply (rule_tac x = "a div m - b div m" in exI)
-  apply (rule_tac m1 = m in aux [THEN trans])
+  apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
   apply auto
   done
 
@@ -688,7 +683,7 @@
 
 declare xzgcda.simps [simp del]
 
-lemma aux1:
+lemma xzgcd_correct_aux1:
   "zgcd (r', r) = k --> 0 < r -->
     (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
   apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
@@ -707,7 +702,7 @@
   apply (simp add: zabs_def)
   done
 
-lemma aux2:
+lemma xzgcd_correct_aux2:
   "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
     zgcd (r', r) = k"
   apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
@@ -729,25 +724,25 @@
     "0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
   apply (unfold xzgcd_def)
   apply (rule iffI)
-   apply (rule_tac [2] aux2 [THEN mp, THEN mp])
-    apply (rule aux1 [THEN mp, THEN mp])
+   apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
+    apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp])
      apply auto
   done
 
 
 text {* \medskip @{term xzgcd} linear *}
 
-lemma aux:
+lemma xzgcda_linear_aux1:
   "(a - r * b) * m + (c - r * d) * (n::int) =
     (a * m + c * n) - r * (b * m + d * n)"
   apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
   done
 
-lemma aux:
+lemma xzgcda_linear_aux2:
   "r' = s' * m + t' * n ==> r = s * m + t * n
     ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
   apply (rule trans)
-   apply (rule_tac [2] aux [symmetric])
+   apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
   apply (simp add: eq_zdiff_eq zmult_commute)
   done
 
@@ -769,7 +764,7 @@
    apply (rule_tac [2] order_le_neq_implies_less)
    apply (rule_tac [2] pos_mod_sign)
     apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
-      s = s and t' = t' and t = t in aux)
+      s = s and t' = t' and t = t in xzgcda_linear_aux2)
       apply auto
   done
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -32,7 +32,7 @@
 
 text {* \medskip @{term [source] inv} *}
 
-lemma aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
+lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
   apply (subst int_int_eq [symmetric])
   apply auto
   done
@@ -44,7 +44,7 @@
   apply (subst zmod_zmult1_eq [symmetric])
   apply (subst zcong_zmod [symmetric])
   apply (subst power_Suc [symmetric])
-  apply (subst aux)
+  apply (subst inv_is_inv_aux)
    apply (erule_tac [2] Little_Fermat)
    apply (erule_tac [2] zdvd_not_zless)
    apply (unfold zprime_def)
@@ -89,7 +89,7 @@
           apply auto
   done
 
-lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
+lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   apply (unfold zcong_def)
   apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -106,7 +106,7 @@
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply auto
-  apply (simp add: aux)
+  apply (simp add: inv_not_p_minus_1_aux)
   apply (subgoal_tac "a = p - 1")
    apply (rule_tac [2] zcong_zless_imp_eq)
        apply auto
@@ -137,7 +137,7 @@
   apply (simp add: pos_mod_bound)
   done
 
-lemma aux: "5 \<le> p ==>
+lemma inv_inv_aux: "5 \<le> p ==>
     nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
   apply (subst int_int_eq [symmetric])
   apply (simp add: zmult_int [symmetric])
@@ -163,7 +163,7 @@
       apply (subst zcong_zmod)
       apply (subst mod_mod_trivial)
       apply (subst zcong_zmod [symmetric])
-      apply (subst aux)
+      apply (subst inv_inv_aux)
        apply (subgoal_tac [2]
 	 "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
         apply (rule_tac [3] zcong_zmult)
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -161,7 +161,7 @@
   from this and b show ?thesis ..
 qed
 
-lemma (in functional_vectorspace) function_norm_least [intro?]:
+lemma (in functional_vectorspace) function_norm_least' [intro?]:
   includes continuous
   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
@@ -234,7 +234,7 @@
   includes continuous
   assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
-proof (rule function_norm_least)
+proof (rule function_norm_least')
   fix b assume b: "b \<in> B V f"
   show "b \<le> c"
   proof cases
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -268,11 +268,11 @@
 b y Clarsimp_tac 1;
 b y ftac BufAC_Asm_d3 1;
 b y Force_tac 1;
-qed "adm_non_BufAC_Asm";
+qed "adm_non_BufAC_Asm'";
 
 Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
 by (rtac triv_admI 1);
 by (Clarify_tac 1);
 by (eatac Buf_Eq_imp_AC_lemma 1 1); 
       (* this is what we originally aimed to show, using admissibilty :-( *)
-qed "adm_BufAC";
+qed "adm_BufAC'";
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/Fix.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -697,10 +697,6 @@
 by (atac 1);
 qed "adm_disj";
 
-
-bind_thm("adm_lemma11",adm_lemma11);
-bind_thm("adm_disj",adm_disj);
-
 Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
 by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
 by (etac ssubst 1);
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/IOA/ABP/Lemmas.ML
--- a/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -6,10 +6,6 @@
 
 (* Logic *)
 
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
 goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
 by (Fast_tac 1);
 val and_de_morgan_and_absorbe = result();
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -6,10 +6,6 @@
 
 (* Logic *)
 
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
 goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
   by (Fast_tac 1);
 qed "fork_lemma";
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/IOA/ex/TrivEx.ML
--- a/src/HOLCF/IOA/ex/TrivEx.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -6,11 +6,6 @@
 Trivial Abstraction Example.
 *)
 
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
-
 Goalw [is_abstraction_def] 
 "is_abstraction h_abs C_ioa A_ioa";
 by (rtac conjI 1);
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/IOA/ex/TrivEx2.ML
--- a/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -6,11 +6,6 @@
 Trivial Abstraction Example.
 *)
 
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
-
 Goalw [is_abstraction_def] 
 "is_abstraction h_abs C_ioa A_ioa";
 by (rtac conjI 1);
diff -r 079af5c90d1c -r 604d0f3622d6 src/HOLCF/ex/loeckx.ML
--- a/src/HOLCF/ex/loeckx.ML	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/ex/loeckx.ML	Tue Aug 27 11:03:05 2002 +0200
@@ -66,7 +66,7 @@
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);
 by (rtac (chain_iterate RS chainE) 1);
-qed "cont_Ifix2";
+qed "cont_Ifix2'";
 
 (* the proof in little steps *)
 
@@ -98,5 +98,5 @@
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);
 by (rtac (chain_iterate RS chainE) 1);
-qed "cont_Ifix2";
+qed "cont_Ifix2''";
 
diff -r 079af5c90d1c -r 604d0f3622d6 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Cardinal.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -892,7 +892,7 @@
 done
 
 (* Induction principle for Finite(A), by Sidi Ehmety *)
-lemma Finite_induct:
+lemma Finite_induct [case_names 0 cons, induct set: Finite]:
 "[| Finite(A); P(0);
     !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
  ==> P(A)"
@@ -900,8 +900,6 @@
 apply (blast intro: Fin_into_Finite)+
 done
 
-lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
-
 (*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
 lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
 apply (unfold Finite_def)
diff -r 079af5c90d1c -r 604d0f3622d6 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Epsilon.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -96,7 +96,7 @@
 done
 
 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
-lemma eclose_induct_down: 
+lemma eclose_induct_down [consumes 1]:
     "[| a: eclose(b);                                            
         !!y.   [| y: b |] ==> P(y);                              
         !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)         
@@ -108,9 +108,6 @@
 apply (blast intro: arg_subset_eclose [THEN subsetD])
 done
 
-(*fixed up for induct method*)
-lemmas eclose_induct_down = eclose_induct_down [consumes 1]
-
 lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
 apply (erule equalityI [OF eclose_least arg_subset_eclose])
 apply (rule subset_refl)
diff -r 079af5c90d1c -r 604d0f3622d6 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Finite.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -56,7 +56,7 @@
 (** Induction on finite sets **)
 
 (*Discharging x~:y entails extra work*)
-lemma Fin_induct:
+lemma Fin_induct [case_names 0 cons, induct set: Fin]:
     "[| b: Fin(A);
         P(0);
         !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
@@ -67,9 +67,6 @@
 apply simp
 done
 
-(*fixed up for induct method*)
-lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
-
 
 (** Simplification for Fin **)
 declare Fin.intros [simp]
diff -r 079af5c90d1c -r 604d0f3622d6 src/ZF/List.thy
--- a/src/ZF/List.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/List.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -425,7 +425,7 @@
 
 (** New induction rules **)
 
-lemma list_append_induct:
+lemma list_append_induct [case_names Nil snoc, consumes 1]:
     "[| l: list(A);
         P(Nil);
         !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
@@ -434,8 +434,6 @@
 apply (erule rev_type [THEN list.induct], simp_all)
 done
 
-lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
-
 lemma list_complete_induct_lemma [rule_format]:
  assumes ih: 
     "\<And>l. [| l \<in> list(A); 
diff -r 079af5c90d1c -r 604d0f3622d6 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Nat.thy	Tue Aug 27 11:03:05 2002 +0200
@@ -79,13 +79,10 @@
 subsection{*Injectivity Properties and Induction*}
 
 (*Mathematical induction*)
-lemma nat_induct:
+lemma nat_induct [case_names 0 succ, induct set: nat]:
     "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
 by (erule def_induct [OF nat_def nat_bnd_mono], blast)
 
-(*fixed up for induct method*)
-lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
-
 lemma natE:
     "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
 by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
@@ -168,7 +165,7 @@
 done
 
 (*Induction suitable for subtraction and less-than*)
-lemma diff_induct: 
+lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
     "[| m: nat;  n: nat;   
         !!x. x: nat ==> P(x,0);   
         !!y. y: nat ==> P(0,succ(y));   
@@ -181,8 +178,6 @@
 apply (erule_tac n=j in nat_induct, auto)  
 done
 
-(*fixed up for induct method*)
-lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
 
 (** Induction principle analogous to trancl_induct **)