dropped aliasses
authorhaftmann
Wed Dec 21 21:26:26 2016 +0100 (2016-12-21)
changeset 646329df24b8b6c0a
parent 64631 7705926ee595
child 64633 5ebcf6c525f1
dropped aliasses
NEWS
src/HOL/Library/Transitive_Closure_Table.thy
src/HOL/Relation.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Wed Dec 21 21:26:25 2016 +0100
     1.2 +++ b/NEWS	Wed Dec 21 21:26:26 2016 +0100
     1.3 @@ -16,6 +16,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Swapped orientation of congruence rules mod_add_left_eq,
    1.11  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.12  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
     2.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Wed Dec 21 21:26:25 2016 +0100
     2.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Wed Dec 21 21:26:26 2016 +0100
     2.3 @@ -207,10 +207,10 @@
     2.4  code_pred rtranclp
     2.5    using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
     2.6  
     2.7 -lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z"
     2.8 +lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> Rangep R z"
     2.9  by(induction rule: rtrancl_path.induct) auto
    2.10  
    2.11 -lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y"
    2.12 +lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> Rangep R y"
    2.13  by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
    2.14  
    2.15  lemma rtrancl_path_nth:
     3.1 --- a/src/HOL/Relation.thy	Wed Dec 21 21:26:25 2016 +0100
     3.2 +++ b/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
     3.3 @@ -1154,7 +1154,4 @@
     3.4  abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
     3.5    where "transP r \<equiv> trans {(x, y). r x y}"  (* FIXME drop *)
     3.6  
     3.7 -abbreviation (input) "RangeP \<equiv> Rangep"
     3.8 -abbreviation (input) "DomainP \<equiv> Domainp"
     3.9 -
    3.10  end
     4.1 --- a/src/HOL/Wellfounded.thy	Wed Dec 21 21:26:25 2016 +0100
     4.2 +++ b/src/HOL/Wellfounded.thy	Wed Dec 21 21:26:26 2016 +0100
     4.3 @@ -308,7 +308,7 @@
     4.4    done
     4.5  
     4.6  lemma wfP_SUP:
     4.7 -  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow>
     4.8 +  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
     4.9      wfP (SUPREMUM UNIV r)"
    4.10    by (rule wf_UN[to_pred]) simp_all
    4.11