# HG changeset patch
# User nipkow
# Date 988983528 -7200
# Node ID 981ea92a86dd603593715e02cd966e366b841531
# Parent  358f82c4550d805225190abd825a81b0a3d97560
made same_fst recdef_simp

diff -r 358f82c4550d -r 981ea92a86dd src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu May 03 18:22:36 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri May 04 15:38:48 2001 +0200
@@ -46,8 +46,8 @@
       then arbitrary
       else if b s then while_aux (b, c, c s)
       else s)"
+thm while_aux.simps
   apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
-   apply (simp add: same_fst_def)
   apply (rule refl)
   done
 
diff -r 358f82c4550d -r 981ea92a86dd src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Thu May 03 18:22:36 2001 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri May 04 15:38:48 2001 +0200
@@ -74,8 +74,6 @@
 apply  auto
 done
 
-declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
-
 consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
         'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
 
@@ -84,8 +82,10 @@
                          | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
       f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
 (hints intro: subcls1I)
+
 declare class_rec.simps [simp del]
 
+
 lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
  class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
   apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
diff -r 358f82c4550d -r 981ea92a86dd src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Thu May 03 18:22:36 2001 +0200
+++ b/src/HOL/Recdef.thy	Fri May 04 15:38:48 2001 +0200
@@ -59,6 +59,7 @@
   inv_image_def
   measure_def
   lex_prod_def
+  same_fst_def
   less_Suc_eq [THEN iffD2]
 
 lemmas [recdef_cong] = if_cong image_cong