diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Tue Sep 20 05:47:11 2011 +0200
+++ b/src/HOL/IMP/VC.thy	Tue Sep 20 05:48:23 2011 +0200
@@ -49,14 +49,14 @@
 subsection "Soundness"
 
 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
-proof(induct c arbitrary: Q)
+proof(induction c arbitrary: Q)
   case (Awhile b I c)
   show ?case
   proof(simp, rule While')
     from `\<forall>s. vc (Awhile b I c) Q s`
     have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
          pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
-    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
+    have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
     with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
       by(rule strengthen_pre)
     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
@@ -72,20 +72,20 @@
 
 lemma pre_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
-proof (induct c arbitrary: P P' s)
+proof (induction c arbitrary: P P' s)
   case Asemi thus ?case by simp metis
 qed simp_all
 
 lemma vc_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
-proof(induct c arbitrary: P P')
+proof(induction c arbitrary: P P')
   case Asemi thus ?case by simp (metis pre_mono)
 qed simp_all
 
 lemma vc_complete:
  "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
   (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
-proof (induct rule: hoare.induct)
+proof (induction rule: hoare.induct)
   case Skip
   show ?case (is "\<exists>ac. ?C ac")
   proof show "?C Askip" by simp qed
@@ -95,8 +95,8 @@
   proof show "?C(Aassign x a)" by simp qed
 next
   case (Semi P c1 Q c2 R)
-  from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
-  from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
+  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
+  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof
     show "?C(Asemi ac1 ac2)"
@@ -104,9 +104,9 @@
   qed
 next
   case (If P b c1 Q c2)
-  from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
+  from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
     by blast
-  from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
+  from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
     by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof
@@ -114,7 +114,7 @@
   qed
 next
   case (While P b c)
-  from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
+  from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   show ?case (is "\<exists>ac. ?C ac")
   proof show "?C(Awhile b P ac)" using ih by simp qed
 next