--- a/src/ZF/Bin.thy Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/Bin.thy Sun May 20 18:45:18 2018 +0200
@@ -652,15 +652,6 @@
(** For cancel_numerals **)
-lemmas rel_iff_rel_0_rls =
- zless_iff_zdiff_zless_0 [where y = "u $+ v"]
- eq_iff_zdiff_eq_0 [where y = "u $+ v"]
- zle_iff_zdiff_zle_0 [where y = "u $+ v"]
- zless_iff_zdiff_zless_0 [where y = n]
- eq_iff_zdiff_eq_0 [where y = n]
- zle_iff_zdiff_zle_0 [where y = n]
- for u v (* FIXME n (!?) *)
-
lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
@@ -673,6 +664,18 @@
apply (simp add: zadd_ac)
done
+context fixes n :: i
+begin
+
+lemmas rel_iff_rel_0_rls =
+ zless_iff_zdiff_zless_0 [where y = "u $+ v"]
+ eq_iff_zdiff_eq_0 [where y = "u $+ v"]
+ zle_iff_zdiff_zle_0 [where y = "u $+ v"]
+ zless_iff_zdiff_zless_0 [where y = n]
+ eq_iff_zdiff_eq_0 [where y = n]
+ zle_iff_zdiff_zle_0 [where y = n]
+ for u v
+
lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
done
@@ -681,6 +684,8 @@
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
done
+end
+
lemma le_add_iff1: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $\<le> n)"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
--- a/src/ZF/Induct/Tree_Forest.thy Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy Sun May 20 18:45:18 2018 +0200
@@ -22,7 +22,7 @@
tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1]
and forest'induct =
tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1]
- for t
+ for t f
declare tree_forest.intros [simp, TC]
--- a/src/ZF/UNITY/Constrains.thy Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/UNITY/Constrains.thy Sun May 20 18:45:18 2018 +0200
@@ -451,7 +451,7 @@
(*Delete the nearest invariance assumption (which will be the second one
used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
+lemmas Always_thin = thin_rl [of "F \<in> Always(A)"] for F A
(*To allow expansion of the program's definition when appropriate*)
named_theorems program "program definitions"
--- a/src/ZF/upair.thy Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/upair.thy Sun May 20 18:45:18 2018 +0200
@@ -230,10 +230,10 @@
**)
lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
-lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
+lemmas split_if_eq2 = split_if [of "%x. a = x"] for a
lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
-lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x
+lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for a
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2