1.1 --- a/thys/Huffman/Huffman.thy Thu Nov 05 16:17:21 2009 +0100
1.2 +++ b/thys/Huffman/Huffman.thy Fri Nov 06 15:02:13 2009 +0100
1.3 @@ -461,7 +461,7 @@
1.4 *}
1.5
1.6 apply rotate_tac
1.7 -apply induct_scheme
1.8 +apply induction_schema
1.9 apply atomize_elim
1.10 apply (case_tac t)
1.11 apply fastsimp
1.12 @@ -1129,7 +1129,7 @@
1.13 P (InnerNode w t\<^isub>1 t\<^isub>2) a\<rbrakk> \<Longrightarrow>
1.14 P t a"
1.15 apply rotate_tac
1.16 -apply induct_scheme
1.17 +apply induction_schema
1.18 apply atomize_elim
1.19 apply (case_tac t, simp)
1.20 apply clarsimp