src/HOL/Library/RBT_Set.thy
changeset 56519 c1048f5bbb45
parent 56218 1c3f1f2431f9
child 56790 f54097170704
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Apr 10 17:48:14 2014 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Apr 10 17:48:15 2014 +0200
     1.3 @@ -640,7 +640,7 @@
     1.4  proof -
     1.5    have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
     1.6      by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
     1.7 -  have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
     1.8 +  have **: "eq_onp is_rbt rbt.Empty rbt.Empty" unfolding eq_onp_def by simp
     1.9    show ?thesis  
    1.10      by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
    1.11  qed
    1.12 @@ -672,7 +672,7 @@
    1.13      fix x :: "'a :: linorder"
    1.14      let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
    1.15      have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
    1.16 -    then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
    1.17 +    then have **:"eq_onp is_rbt ?t ?t" unfolding eq_onp_def by auto
    1.18  
    1.19      have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
    1.20        by (subst(asm) RBT_inverse[symmetric, OF *])