--- a/src/HOL/Data_Structures/AA_Set.thy Sat Mar 05 23:05:07 2016 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Sun Mar 06 10:33:34 2016 +0100
@@ -120,10 +120,10 @@
by(cases t) auto
lemma lvl_skew: "lvl (skew t) = lvl t"
-by(induction t rule: skew.induct) auto
+by(cases t rule: skew.cases) auto
lemma lvl_split: "lvl (split t) = lvl t \<or> lvl (split t) = lvl t + 1 \<and> sngl (split t)"
-by(induction t rule: split.induct) auto
+by(cases t rule: split.cases) auto
lemma invar_2Nodes:"invar (Node lv l x (Node rlv rl rx rr)) =
(invar l \<and> invar \<langle>rlv, rl, rx, rr\<rangle> \<and> lv = Suc (lvl l) \<and>
@@ -155,7 +155,7 @@
using lvl_insert_aux by blast
lemma lvl_insert_sngl: "invar t \<Longrightarrow> sngl t \<Longrightarrow> lvl(insert x t) = lvl t"
-proof (induction t rule: "insert.induct" )
+proof (induction t rule: insert.induct)
case (2 x lv t1 a t2)
consider (LT) "x < a" | (GT) "x > a" | (EQ) "x = a"
using less_linear by blast
@@ -174,10 +174,10 @@
qed simp
lemma skew_invar: "invar t \<Longrightarrow> skew t = t"
-by(induction t rule: skew.induct) auto
+by(cases t rule: skew.cases) auto
lemma split_invar: "invar t \<Longrightarrow> split t = t"
-by(induction t rule: split.induct) clarsimp+
+by(cases t rule: split.cases) clarsimp+
lemma invar_NodeL:
"\<lbrakk> invar(Node n l x r); invar l'; lvl l' = lvl l \<rbrakk> \<Longrightarrow> invar(Node n l' x r)"
@@ -468,7 +468,7 @@
subsubsection "Proofs for delete"
lemma inorder_adjust: "t \<noteq> Leaf \<Longrightarrow> pre_adjust t \<Longrightarrow> inorder(adjust t) = inorder t"
-by(induction t)
+by(cases t)
(auto simp: adjust_def inorder_skew inorder_split invar.simps(2) pre_adjust.simps
split: tree.splits)