# HG changeset patch
# User paulson
# Date 903622719 -7200
# Node ID 5f6416d64a947dc4fc3af6d085950a567a4738cf
# Parent  d014d7e57337df6cff29fe82b96d14192cc34042
Must remove less_imp_le from simpset

diff -r d014d7e57337 -r 5f6416d64a94 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Thu Aug 20 10:17:18 1998 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Aug 20 16:18:39 1998 +0200
@@ -8,7 +8,7 @@
 
 open W;
 
-Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
+Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
 
 val has_type_casesE = map(has_type.mk_cases expr.simps)
         [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];
diff -r d014d7e57337 -r 5f6416d64a94 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Thu Aug 20 10:17:18 1998 +0200
+++ b/src/HOL/W0/W.ML	Thu Aug 20 16:18:39 1998 +0200
@@ -6,7 +6,8 @@
 Correctness and completeness of type inference algorithm W
 *)
 
-Addsimps [Suc_le_lessD];
+Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
+
 Delsimps (ex_simps @ all_simps);
 
 (* correctness of W with respect to has_type *)
@@ -82,8 +83,7 @@
 
 
 (* resulting type variable is new *)
-Goal
-     "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
+Goal "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
 \                 new_tv m s & new_tv m t";
 by (induct_tac "e" 1);
 (* case Var n *)
@@ -213,8 +213,7 @@
 qed_spec_mp "free_tv_W"; 
 
 (* Completeness of W w.r.t. has_type *)
-Goal
- "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
+Goal "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
 \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
 \                     (? r. $s' a = $r ($s a) & t' = $r t))";
 by (induct_tac "e" 1);