# HG changeset patch
# User haftmann
# Date 1560501267 0
# Node ID e939ea997f5fc2c99d6525e3f876a7b13c009c28
# Parent  c832d431636b3b7871d62c2f8dbd0a7393f42c04
dropped weaker legacy alias

diff -r c832d431636b -r e939ea997f5f src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -1016,14 +1016,4 @@
   "drop_bit n (Suc 0) = of_bool (n = 0)"
   using drop_bit_of_1 [where ?'a = nat] by simp
 
-
-subsection \<open>Legacy\<close>
-
-lemma parity_induct [case_names zero even odd]:
-  assumes zero: "P 0"
-  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
-  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
-  shows "P n"
-  using assms by (rule nat_parity_induct)
-
 end
diff -r c832d431636b -r e939ea997f5f src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -61,12 +61,12 @@
 
 lemma not_last_bits_of_nat [simp]:
   "\<not> last (bits_of (of_nat n))"
-  by (induction n rule: parity_induct)
+  by (induction n rule: nat_parity_induct)
     (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
 
 lemma of_unsigned_bits_of_nat:
   "of_unsigned (bits_of (of_nat n)) = of_nat n"
-  by (induction n rule: parity_induct)
+  by (induction n rule: nat_parity_induct)
     (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
 
 end
@@ -106,7 +106,7 @@
 
 lemma last_bits_of_neg_of_nat [simp]:
   "last (bits_of (- 1 - of_nat n))"
-proof (induction n rule: parity_induct)
+proof (induction n rule: nat_parity_induct)
   case zero
   then show ?case
     by simp
@@ -132,7 +132,7 @@
   "of_signed (bits_of (- 1 - of_nat n)) = - 1 - of_nat n"
 proof -
   have "of_unsigned (map Not (bits_of (- 1 - of_nat n))) = of_nat n"
-  proof (induction n rule: parity_induct)
+  proof (induction n rule: nat_parity_induct)
     case zero
     then show ?case
       by simp