--- 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
--- 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]]])
--- 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