--- 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
--- 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