src/HOLCF/IMP/Denotational.ML

  "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
 by (simp_tac (simpset() addsplits [split_lift_case]) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
-Goal "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
+Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
 by (etac evalc.induct 1);
       by (ALLGOALS Asm_simp_tac);
  by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
 qed_spec_mp "eval_implies_D";