src/HOL/OrderedGroup.thy
changeset 28823 dcbef866c9e2
parent 28262 aa7ca36d67fd
child 29269 5c25a2012975
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  begin
     1.5  
     1.6  subclass monoid_add
     1.7 -  by unfold_locales (insert add_0, simp_all add: add_commute)
     1.8 +  proof qed (insert add_0, simp_all add: add_commute)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -99,7 +99,7 @@
    1.13  begin
    1.14  
    1.15  subclass monoid_mult
    1.16 -  by unfold_locales (insert mult_1, simp_all add: mult_commute)
    1.17 +  proof qed (insert mult_1, simp_all add: mult_commute)
    1.18  
    1.19  end
    1.20  
    1.21 @@ -123,7 +123,7 @@
    1.22  begin
    1.23  
    1.24  subclass cancel_semigroup_add
    1.25 -proof unfold_locales
    1.26 +proof
    1.27    fix a b c :: 'a
    1.28    assume "a + b = a + c" 
    1.29    then show "b = c" by (rule add_imp_eq)
    1.30 @@ -248,10 +248,10 @@
    1.31  begin
    1.32  
    1.33  subclass group_add
    1.34 -  by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
    1.35 +  proof qed (simp_all add: ab_left_minus ab_diff_minus)
    1.36  
    1.37  subclass cancel_ab_semigroup_add
    1.38 -proof unfold_locales
    1.39 +proof
    1.40    fix a b c :: 'a
    1.41    assume "a + b = a + c"
    1.42    then have "- a + a + b = - a + a + c"
    1.43 @@ -490,7 +490,7 @@
    1.44  subclass pordered_cancel_ab_semigroup_add ..
    1.45  
    1.46  subclass pordered_ab_semigroup_add_imp_le
    1.47 -proof unfold_locales
    1.48 +proof
    1.49    fix a b c :: 'a
    1.50    assume "c + a \<le> c + b"
    1.51    hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
    1.52 @@ -646,7 +646,7 @@
    1.53  subclass ordered_ab_semigroup_add ..
    1.54  
    1.55  subclass pordered_ab_semigroup_add_imp_le
    1.56 -proof unfold_locales
    1.57 +proof
    1.58    fix a b c :: 'a
    1.59    assume le: "c + a <= c + b"  
    1.60    show "a <= b"
    1.61 @@ -1243,7 +1243,7 @@
    1.62    have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
    1.63      by (simp add: abs_lattice le_supI)
    1.64    show ?thesis
    1.65 -  proof unfold_locales
    1.66 +  proof
    1.67      fix a
    1.68      show "0 \<le> \<bar>a\<bar>" by simp
    1.69    next