src/HOL/MiniML/MiniML.thy

removed make_chart;
theories are now read from the current directory (because of use_dir)

(* 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