| changeset 1376 | 92f83b9d17e1 |
| parent 1300 | c7a8f374339b |
| child 1400 | 5d909faf0e04 |
--- a/src/HOL/MiniML/I.thy Thu Nov 30 12:58:44 1995 +0100 +++ b/src/HOL/MiniML/I.thy Fri Dec 01 12:03:13 1995 +0100 @@ -8,7 +8,7 @@ I = W + consts - I :: "[expr, type_expr list, nat, subst] => result_W" + I :: [expr, type_expr list, nat, subst] => result_W primrec I expr I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)