src/HOL/ex/LList.ML

 
 (*Surprisingly hard to prove.  Used with lfilter*)
 goalw thy [llistD_Fun_def, prod_fun_def]
     "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
 by (Auto_tac());
-br image_eqI 1;
+by (rtac image_eqI 1);
 by (fast_tac (!claset addss (!simpset)) 1);
 by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
 qed "llistD_Fun_mono";
 
 (** To show two llists are equal, exhibit a bisimulation!