1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Mon Nov 24 18:04:21 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Mon Nov 24 18:05:20 2008 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  locale param1 = fixes p
     1.5  print_locale! param1
     1.6  
     1.7 -locale param2 = fixes p :: 'a
     1.8 +locale param2 = fixes p :: 'b
     1.9  print_locale! param2
    1.10  
    1.11  (*
    1.12 @@ -54,7 +54,7 @@
    1.13  print_locale! constraint2
    1.14  
    1.15  
    1.16 -text {* Groups *}
    1.17 +text {* Inheritance *}
    1.18  
    1.19  locale semi =
    1.20    fixes prod (infixl "**" 65)
    1.21 @@ -91,7 +91,7 @@
    1.22  print_locale! pert_hom' thm pert_hom'_def
    1.23  
    1.24  
    1.25 -text {* Logic *}
    1.26 +text {* Syntax declarations *}
    1.27  
    1.28  locale logic =
    1.29    fixes land (infixl "&&" 55)
    1.30 @@ -109,7 +109,9 @@
    1.31  locale use_decl = logic + semi "op ||"
    1.32  print_locale! use_decl thm use_decl_def
    1.33  
    1.34 -(*
    1.35 +
    1.36 +text {* Theorem statements *}
    1.37 +
    1.38  lemma (in lgrp) lcancel:
    1.39    "x ** y = x ** z <-> y = z"
    1.40  proof
    1.41 @@ -117,15 +119,16 @@
    1.42    then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
    1.43    then show "y = z" by (simp add: lone linv)
    1.44  qed simp
    1.45 -*)
    1.46 +print_locale! lgrp
    1.47 +
    1.48  
    1.49  locale rgrp = semi +
    1.50    fixes one and inv
    1.51    assumes rone: "x ** one = x"
    1.52      and rinv: "x ** inv(x) = one"
    1.53 +begin
    1.54  
    1.55 -(*
    1.56 -lemma (in rgrp) rcancel:
    1.57 +lemma rcancel:
    1.58    "y ** x = z ** x <-> y = z"
    1.59  proof
    1.60    assume "y ** x = z ** x"
    1.61 @@ -133,7 +136,8 @@
    1.62      by (simp add: assoc [symmetric])
    1.63    then show "y = z" by (simp add: rone rinv)
    1.64  qed simp
    1.65 -*)
    1.66 -
    1.67  
    1.68  end
    1.69 +print_locale! rgrp
    1.70 +
    1.71 +end