--- a/src/HOL/MiniML/MiniML.thy Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/MiniML.thy Fri Dec 08 19:48:15 1995 +0100
@@ -14,9 +14,9 @@
(* type inference rules *)
consts
- has_type :: "(type_expr list * expr * type_expr)set"
+ has_type :: "(typ list * expr * typ)set"
syntax
- "@has_type" :: [type_expr list, expr, type_expr] => bool
+ "@has_type" :: [typ list, expr, typ] => bool
("((_) |-/ (_) :: (_))" 60)
translations
"a |- e :: t" == "(a,e,t):has_type"
@@ -24,8 +24,8 @@
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 |]
+ AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+ AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
==> a |- App e1 e2 :: t1"
end