src/HOL/MiniML/MiniML.thy

+(* 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 :: "(type_expr list * expr * type_expr)set"
+syntax
+        "@has_type" :: "[type_expr list, expr, type_expr] => bool"
+                       ("((_) |-/ (_) :: (_))" 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 :: Fun t1 t2"
+	AppI "[| a |- e1 :: Fun t2 t1; a |- e2 :: t2 |] 
+     	      ==> a |- App e1 e2 :: t1"
+
+end
+