src/HOL/MicroJava/Comp/Index.thy

--- a/src/HOL/MicroJava/Comp/Index.thy	Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy	Mon May 26 18:36:15 2003 +0200
@@ -63,6 +63,10 @@
 apply simp
 done
 
+lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))"
+apply auto
+done
+
 lemma update_at_index: "
   \<lbrakk> distinct (gjmb_plns (gmb G C S)); 
   x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>