# HG changeset patch
# User wenzelm
# Date 1525726104 -7200
# Node ID 3687109009c4ebe6d711c7cb6539abb7e69724c7
# Parent  b2d84b1114face1091e8c84f595a07d64da5bc22# Parent  a514e29db9806aa874b80e4e1ebbba9e0b29f913
merged

diff -r a514e29db980 -r 3687109009c4 NEWS
--- 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 ***
 
diff -r a514e29db980 -r 3687109009c4 src/HOL/Divides.thy
--- 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
diff -r a514e29db980 -r 3687109009c4 src/HOL/Groebner_Basis.thy
--- 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
diff -r a514e29db980 -r 3687109009c4 src/HOL/Presburger.thy
--- 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]
 
diff -r a514e29db980 -r 3687109009c4 src/HOL/Tools/string_syntax.ML
--- 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"},
diff -r a514e29db980 -r 3687109009c4 src/HOL/Transcendental.thy
--- 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
diff -r a514e29db980 -r 3687109009c4 src/Pure/Isar/class.ML
--- 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