--- a/NEWS Mon May 07 19:40:55 2018 +0200
+++ b/NEWS Mon May 07 22:48:24 2018 +0200
@@ -278,10 +278,6 @@
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
INCOMPATIBILITY.
-* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid
-clash with fact mod_mult_self4 (on more generic semirings).
-INCOMPATIBILITY.
-
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
interpretation of abstract locales. INCOMPATIBILITY.
@@ -318,6 +314,18 @@
* Code generation: Code generation takes an explicit option
"case_insensitive" to accomodate case-insensitive file systems.
+* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
+clash with fact mod_mult_self4 (on more generic semirings).
+INCOMPATIBILITY.
+
+* Eliminated some theorem aliasses:
+
+ even_times_iff ~> even_mult_iff
+ mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
+ even_of_nat ~> even_int_iff
+
+INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Divides.thy Mon May 07 19:40:55 2018 +0200
+++ b/src/HOL/Divides.thy Mon May 07 22:48:24 2018 +0200
@@ -1295,10 +1295,6 @@
subsubsection \<open>Lemmas of doubtful value\<close>
-lemma mod_mult_self3':
- "Suc (k * n + m) mod n = Suc m mod n"
- by (fact Suc_mod_mult_self3)
-
lemma mod_Suc_eq_Suc_mod:
"Suc m mod n = Suc (m mod n) mod n"
by (simp add: mod_simps)
@@ -1327,16 +1323,6 @@
then show ?thesis ..
qed
-lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close>
-
-lemma mod_2_not_eq_zero_eq_one_nat:
- fixes n :: nat
- shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
- by (fact not_mod_2_eq_0_eq_1)
-
-lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
- by (fact even_of_nat)
-
lemma is_unit_int:
"is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
by auto
--- a/src/HOL/Groebner_Basis.thy Mon May 07 19:40:55 2018 +0200
+++ b/src/HOL/Groebner_Basis.thy Mon May 07 22:48:24 2018 +0200
@@ -78,7 +78,7 @@
context semiring_parity
begin
-declare even_times_iff [algebra]
+declare even_mult_iff [algebra]
declare even_power [algebra]
end
--- a/src/HOL/Presburger.thy Mon May 07 19:40:55 2018 +0200
+++ b/src/HOL/Presburger.thy Mon May 07 22:48:24 2018 +0200
@@ -435,7 +435,7 @@
context semiring_parity
begin
-declare even_times_iff [presburger]
+declare even_mult_iff [presburger]
declare even_power [presburger]
--- a/src/HOL/Tools/string_syntax.ML Mon May 07 19:40:55 2018 +0200
+++ b/src/HOL/Tools/string_syntax.ML Mon May 07 22:48:24 2018 +0200
@@ -117,7 +117,7 @@
c $ string_tr [t] $ u
| string_tr [Free (str, _)] =
mk_string_syntax (plain_strings_of str)
- | string_tr ts = raise TERM ("char_tr", ts);
+ | string_tr ts = raise TERM ("string_tr", ts);
fun list_ast_tr' [args] =
Ast.Appl [Ast.Constant @{syntax_const "_String"},
--- a/src/HOL/Transcendental.thy Mon May 07 19:40:55 2018 +0200
+++ b/src/HOL/Transcendental.thy Mon May 07 22:48:24 2018 +0200
@@ -4173,10 +4173,10 @@
lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
proof safe
assume "cos x = 0"
- then show "\<exists>n. odd n \<and> x = of_int n * (pi/2)"
- apply (simp add: cos_zero_iff)
- apply safe
- apply (metis even_int_iff of_int_of_nat_eq)
+ then show "\<exists>n. odd n \<and> x = of_int n * (pi / 2)"
+ unfolding cos_zero_iff
+ apply (auto simp add: cos_zero_iff)
+ apply (metis even_of_nat of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI)
apply simp
done
@@ -4196,7 +4196,7 @@
then show "\<exists>n. even n \<and> x = of_int n * (pi / 2)"
apply (simp add: sin_zero_iff)
apply safe
- apply (metis even_int_iff of_int_of_nat_eq)
+ apply (metis even_of_nat of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI)
apply simp
done
--- a/src/Pure/Isar/class.ML Mon May 07 19:40:55 2018 +0200
+++ b/src/Pure/Isar/class.ML Mon May 07 22:48:24 2018 +0200
@@ -196,13 +196,13 @@
([Pretty.keyword1 "class", Pretty.brk 1,
Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
- (case try (Axclass.get_info thy) class of
- NONE => []
- | SOME {params, ...} =>
+ (case (these o Option.map #params o try (Axclass.get_info thy)) class of
+ [] => []
+ | params =>
[Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
- (case Symtab.lookup arities class of
- NONE => []
- | SOME ars =>
+ (case (these o Symtab.lookup arities) class of
+ [] => []
+ | ars =>
[Pretty.fbrk, Pretty.big_list "instances:"
(map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))]));
in