equal
deleted
inserted
replaced
872 |
872 |
873 @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]} |
873 @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]} |
874 |
874 |
875 They can be removed anywhere if the relation is an equivalence relation: |
875 They can be removed anywhere if the relation is an equivalence relation: |
876 |
876 |
877 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
877 @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]} |
878 |
878 |
879 And finally it can be removed anywhere if @{term R2} is an equivalence relation: |
879 And finally it can be removed anywhere if @{term R2} is an equivalence relation: |
880 |
880 |
881 @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]} |
881 @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]} |
882 |
882 |