--- a/src/HOL/MiniML/I.thy Fri Jan 17 18:32:24 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: MiniML.thy
- Author: Thomas Stauner
- Copyright 1995 TU Muenchen
-
- Recursive definition of type inference algorithm I for Mini_ML.
-*)
-
-I = W +
-
-consts
- I :: [expr, typ list, nat, subst] => result_W
-
-primrec I expr
- "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
- else Fail)"
- "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
- Ok(s, TVar n -> t, m) )"
- "I (App e1 e2) a n s =
- ( (s1,t1,m1) := I e1 a n s;
- (s2,t2,m2) := I e2 a m1 s1;
- u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
- Ok($u o s2, TVar m2, Suc m2) )"
-end