src/HOL/ex/MT.ML

 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
 qed "hasty_rel_elim";
 
 (* Introduction rules for hasty *)
 
-Goalw [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
+Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
 by (etac hasty_rel_const_coind 1);
 qed "hasty_const";
 
 Goalw [hasty_def,hasty_env_def] 
  "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";

   "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
 by (rtac hasty_rel_elim 1);
 by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
 qed "hasty_elim_const_lem";
 
-Goal "!!c. v_const(c) hasty t ==> c isof t";
+Goal "v_const(c) hasty t ==> c isof t";
 by (dtac hasty_elim_const_lem 1);
 by (Blast_tac 1);
 qed "hasty_elim_const";
 
 (* Elimination on closures for hasty *)