diff -r 2af078382853 -r bee082efaa46 src/HOL/W0/MiniML.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/W0/MiniML.thy	Fri Jan 17 13:21:54 1997 +0100
@@ -0,0 +1,32 @@
+(* Title:     HOL/MiniML/MiniML.thy
+   ID:        $Id$
+   Author:    Dieter Nazareth and Tobias Nipkow
+   Copyright  1995 TU Muenchen
+
+Mini_ML with type inference rules.
+*)
+
+MiniML = Type + 
+
+(* expressions *)
+datatype
+        expr = Var nat | Abs expr | App expr expr
+
+(* type inference rules *)
+consts
+        has_type :: "(typ list * expr * typ)set"
+syntax
+        "@has_type" :: [typ list, expr, typ] => bool
+                       ("((_) |-/ (_) :: (_))" [60,0,60] 60)
+translations 
+        "a |- e :: t" == "(a,e,t):has_type"
+
+inductive has_type
+intrs
+        VarI "[| n < length a |] ==> a |- Var n :: nth n a"
+        AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+        AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
+              ==> a |- App e1 e2 :: t1"
+
+end
+