--- 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" ];
--- 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);