src/HOL/Groups.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 62347 2230b7047376
     1.1 --- a/src/HOL/Groups.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Groups.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -1203,13 +1203,7 @@
     1.4  end
     1.5  
     1.6  class abs =
     1.7 -  fixes abs :: "'a \<Rightarrow> 'a"
     1.8 -begin
     1.9 -
    1.10 -notation (xsymbols)
    1.11 -  abs  ("\<bar>_\<bar>")
    1.12 -
    1.13 -end
    1.14 +  fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
    1.15  
    1.16  class sgn =
    1.17    fixes sgn :: "'a \<Rightarrow> 'a"
    1.18 @@ -1375,7 +1369,7 @@
    1.19  lemma dense_eq0_I:
    1.20    fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
    1.21    shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
    1.22 -  apply (cases "abs x=0", simp)
    1.23 +  apply (cases "\<bar>x\<bar> = 0", simp)
    1.24    apply (simp only: zero_less_abs_iff [symmetric])
    1.25    apply (drule dense)
    1.26    apply (auto simp add: not_less [symmetric])