changeset 4502 | 337c073de95e |
parent 2520 | aecaa76e7eff |
--- a/src/HOL/W0/MiniML.thy Mon Dec 29 21:39:22 1997 +0100 +++ b/src/HOL/W0/MiniML.thy Tue Dec 30 11:14:09 1997 +0100 @@ -23,7 +23,7 @@ inductive has_type intrs - VarI "[| n < length a |] ==> a |- Var n :: nth n a" + VarI "[| n < length a |] ==> a |- Var n :: a!n" AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2" AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] ==> a |- App e1 e2 :: t1"