# HG changeset patch
# User haftmann
# Date 1482351986 -3600
# Node ID 9df24b8b6c0aaa3a1130dc4cf6a4dc88e692ed00
# Parent  7705926ee595daae6a14573f8dd92fe6528e274b
dropped aliasses

diff -r 7705926ee595 -r 9df24b8b6c0a NEWS
--- 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,
diff -r 7705926ee595 -r 9df24b8b6c0a src/HOL/Library/Transitive_Closure_Table.thy
--- 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:
diff -r 7705926ee595 -r 9df24b8b6c0a src/HOL/Relation.thy
--- 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
diff -r 7705926ee595 -r 9df24b8b6c0a src/HOL/Wellfounded.thy
--- 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