author | nipkow |
Mon, 25 Mar 1996 08:46:02 +0100 | |
changeset 1604 | cff41d1094ad |
parent 1603 | 44bc1417b07c |
child 1605 | 248e1e125ca0 |
--- a/src/HOL/MiniML/Type.thy Sun Mar 24 18:36:28 1996 +0100 +++ b/src/HOL/MiniML/Type.thy Mon Mar 25 08:46:02 1996 +0100 @@ -36,9 +36,10 @@ consts app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") -rules - app_subst_TVar "$ s (TVar n) = s n" - app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" +primrec app_subst typ + app_subst_TVar "$ s (TVar n) = s n" + app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" + defs app_subst_list "$ s == map ($ s)"