changeset 1525 | d127436567d0 |
parent 1521 | 4ed3004ff75e |
child 1743 | f7feaacd33d3 |
--- a/src/HOL/MiniML/MiniML.ML Wed Feb 28 11:47:30 1996 +0100 +++ b/src/HOL/MiniML/MiniML.ML Wed Feb 28 16:57:14 1996 +0100 @@ -12,7 +12,7 @@ (* has_type is closed w.r.t. substitution *) goal MiniML.thy - "!a e t. (a |- e :: t) --> ($ s a |- e :: $ s t)"; + "!a e t. a |- e :: t --> $s a |- e :: $s t"; by (rtac has_type.mutual_induct 1); (* case VarI *) by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);