1.1 --- a/src/HOL/MiniML/W.ML	Thu Aug 20 10:17:18 1998 +0200
     1.2 +++ b/src/HOL/MiniML/W.ML	Thu Aug 20 16:18:39 1998 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  open W;
     1.6  
     1.7 -Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
     1.8 +Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
     1.9  
    1.10  val has_type_casesE = map(has_type.mk_cases expr.simps)
    1.11          [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];

     2.1 --- a/src/HOL/W0/W.ML	Thu Aug 20 10:17:18 1998 +0200
     2.2 +++ b/src/HOL/W0/W.ML	Thu Aug 20 16:18:39 1998 +0200
     2.3 @@ -6,7 +6,8 @@
     2.4  Correctness and completeness of type inference algorithm W
     2.5  *)
     2.6  
     2.7 -Addsimps [Suc_le_lessD];
     2.8 +Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
     2.9 +
    2.10  Delsimps (ex_simps @ all_simps);
    2.11  
    2.12  (* correctness of W with respect to has_type *)
    2.13 @@ -82,8 +83,7 @@
    2.14  
    2.15  
    2.16  (* resulting type variable is new *)
    2.17 -Goal
    2.18 -     "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
    2.19 +Goal "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
    2.20  \                 new_tv m s & new_tv m t";
    2.21  by (induct_tac "e" 1);
    2.22  (* case Var n *)
    2.23 @@ -213,8 +213,7 @@
    2.24  qed_spec_mp "free_tv_W"; 
    2.25  
    2.26  (* Completeness of W w.r.t. has_type *)
    2.27 -Goal
    2.28 - "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
    2.29 +Goal "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
    2.30  \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
    2.31  \                     (? r. $s' a = $r ($s a) & t' = $r t))";
    2.32  by (induct_tac "e" 1);