src/HOL/W0/MiniML.ML

 Addsimps has_type.intrs;
 Addsimps [Un_upper1,Un_upper2];
 
 
 (* has_type is closed w.r.t. substitution *)
-Goal "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+Goal "a |- e :: t ==> $s a |- e :: $s t";
 by (etac has_type.induct 1);
 (* case VarI *)
 by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
 by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
 by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (simpset() delsimps [nth_map])) 1);