Updated for new form of induction rules

--- a/src/HOL/IMP/VC.ML	Thu May 09 11:46:32 1996 +0200
+++ b/src/HOL/IMP/VC.ML	Fri May 10 17:03:17 1996 +0200
@@ -55,9 +55,9 @@
 qed_spec_mp "vc_mono";
 
 goal VC.thy
-  "!P c Q. |- {P}c{Q} --> \
+  "!!P c Q. |- {P}c{Q} ==> \
 \          (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))";
-by (rtac hoare.mutual_induct 1);
+by (etac hoare.induct 1);
      by(res_inst_tac [("x","Askip")] exI 1);
      by(Simp_tac 1);
     by(res_inst_tac [("x","Aass x a")] exI 1);
@@ -70,13 +70,13 @@
   by(res_inst_tac [("x","Aif b ac aca")] exI 1);
   by(Asm_simp_tac 1);
  by(SELECT_GOAL(safe_tac HOL_cs)1);
- by(res_inst_tac [("x","Awhile b P ac")] exI 1);
+ by(res_inst_tac [("x","Awhile b Pa ac")] exI 1);
  by(Asm_simp_tac 1);
-by(SELECT_GOAL(safe_tac HOL_cs)1);
+by (safe_tac HOL_cs);
 by(res_inst_tac [("x","ac")] exI 1);
 by(Asm_simp_tac 1);
 by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
-qed_spec_mp "vc_complete";
+qed "vc_complete";
 
 goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
 by(acom.induct_tac "c" 1);

--- 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";