src/HOL/Relation_Power.thy
changeset 20503 503ac4c5ef91
parent 18398 5d63a8b35688
child 21414 4cb808163adc
--- a/src/HOL/Relation_Power.thy	Mon Sep 11 14:35:30 2006 +0200
+++ b/src/HOL/Relation_Power.thy	Mon Sep 11 21:35:19 2006 +0200
@@ -59,7 +59,7 @@
 
 lemma rel_pow_Suc_I2:
     "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
-  apply (induct n fixing: z)
+  apply (induct n arbitrary: z)
    apply simp
   apply fastsimp
   done
@@ -79,7 +79,7 @@
 
 lemma rel_pow_Suc_D2:
     "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
-  apply (induct n fixing: x z)
+  apply (induct n arbitrary: x z)
    apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
   apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
   done