src/HOL/MiniML/MiniML.ML
changeset 1743 f7feaacd33d3
parent 1525 d127436567d0
child 2031 03a843f0f447
--- a/src/HOL/MiniML/MiniML.ML	Thu May 09 11:46:32 1996 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Fri May 10 17:03:17 1996 +0200
@@ -11,9 +11,8 @@
 
 
 (* has_type is closed w.r.t. substitution *)
-goal MiniML.thy
-     "!a e t. a |- e :: t --> $s a |- e :: $s t";
-by (rtac has_type.mutual_induct 1);
+goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+by (etac has_type.induct 1);
 (* case VarI *)
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
 by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
@@ -22,4 +21,4 @@
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
 (* case AppI *)
 by (Asm_full_simp_tac 1);
-qed_spec_mp "has_type_cl_sub";
+qed "has_type_cl_sub";