--- a/NEWS Wed Dec 21 21:26:25 2016 +0100
+++ b/NEWS Wed Dec 21 21:26:26 2016 +0100
@@ -16,6 +16,9 @@
*** HOL ***
+* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
+INCOMPATIBILITY.
+
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
--- a/src/HOL/Library/Transitive_Closure_Table.thy Wed Dec 21 21:26:25 2016 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Wed Dec 21 21:26:26 2016 +0100
@@ -207,10 +207,10 @@
code_pred rtranclp
using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
-lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z"
+lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> Rangep R z"
by(induction rule: rtrancl_path.induct) auto
-lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y"
+lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> Rangep R y"
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
lemma rtrancl_path_nth:
--- a/src/HOL/Relation.thy Wed Dec 21 21:26:25 2016 +0100
+++ b/src/HOL/Relation.thy Wed Dec 21 21:26:26 2016 +0100
@@ -1154,7 +1154,4 @@
abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
where "transP r \<equiv> trans {(x, y). r x y}" (* FIXME drop *)
-abbreviation (input) "RangeP \<equiv> Rangep"
-abbreviation (input) "DomainP \<equiv> Domainp"
-
end
--- a/src/HOL/Wellfounded.thy Wed Dec 21 21:26:25 2016 +0100
+++ b/src/HOL/Wellfounded.thy Wed Dec 21 21:26:26 2016 +0100
@@ -308,7 +308,7 @@
done
lemma wfP_SUP:
- "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow>
+ "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
wfP (SUPREMUM UNIV r)"
by (rule wf_UN[to_pred]) simp_all