# HG changeset patch
# User haftmann
# Date 1593679743 0
# Node ID ec17263ec38dd6c038d63b63efbd00a6ee0023d9
# Parent  76193dd4aec8440ff35f89ef25522cd85b7c0b06
removed superfluous dependency

diff -r 76193dd4aec8 -r ec17263ec38d NEWS
--- a/NEWS	Wed Jul 01 17:32:11 2020 +0000
+++ b/NEWS	Thu Jul 02 08:49:03 2020 +0000
@@ -74,6 +74,9 @@
 "bintrunc" and "max_word" are now mere input abbreviations.
 Minor INCOMPATIBILITY.
 
+* Session HOL-Word: Theory Z2 is not used any longer.
+Minor INCOMPATIBILITY.
+
 * Rewrite rule subst_all performs
 more aggressive substitution with variables from assumptions.
 INCOMPATIBILITY, use something like
diff -r 76193dd4aec8 -r ec17263ec38d src/HOL/Word/Misc_Arithmetic.thy
--- a/src/HOL/Word/Misc_Arithmetic.thy	Wed Jul 01 17:32:11 2020 +0000
+++ b/src/HOL/Word/Misc_Arithmetic.thy	Thu Jul 02 08:49:03 2020 +0000
@@ -3,7 +3,7 @@
 section \<open>Miscellaneous lemmas, mostly for arithmetic\<close>
 
 theory Misc_Arithmetic
-  imports Misc_Auxiliary "HOL-Library.Z2"
+  imports Misc_Auxiliary
 begin
 
 lemma one_mod_exp_eq_one [simp]:
@@ -419,17 +419,4 @@
 
 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
 
-lemma not_B1_is_B0: "y \<noteq> 1 \<Longrightarrow> y = 0"
-  for y :: bit
-  by (cases y) auto
-
-lemma B1_ass_B0:
-  fixes y :: bit
-  assumes y: "y = 0 \<Longrightarrow> y = 1"
-  shows "y = 1"
-  apply (rule classical)
-  apply (drule not_B1_is_B0)
-  apply (erule y)
-  done
-
 end