src/FOL/ex/NewLocaleTest.thy

 text {* Inference of parameter types *}
 
 locale param1 = fixes p
 print_locale! param1
 
-locale param2 = fixes p :: 'a
+locale param2 = fixes p :: 'b
 print_locale! param2
 
 (*
 locale param_top = param2 r for r :: "'b :: {}"
 print_locale! param_top

   fixes p and q
   assumes "p = q"
 print_locale! constraint2
 
 
-text {* Groups *}
+text {* Inheritance *}
 
 locale semi =
   fixes prod (infixl "**" 65)
   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
     and comm: "x ** y = y ** x"

 text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
 locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
 print_locale! pert_hom' thm pert_hom'_def
 
 
-text {* Logic *}
+text {* Syntax declarations *}
 
 locale logic =
   fixes land (infixl "&&" 55)
     and lnot ("-- _" [60] 60)
   assumes assoc: "(x && y) && z = x && (y && z)"

 print_locale! logic
 
 locale use_decl = logic + semi "op ||"
 print_locale! use_decl thm use_decl_def
 
-(*
+
+text {* Theorem statements *}
+
 lemma (in lgrp) lcancel:
   "x ** y = x ** z <-> y = z"
 proof
   assume "x ** y = x ** z"
   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   then show "y = z" by (simp add: lone linv)
 qed simp
-*)
+print_locale! lgrp
+
 
 locale rgrp = semi +
   fixes one and inv
   assumes rone: "x ** one = x"
     and rinv: "x ** inv(x) = one"
+begin
 
-(*
-lemma (in rgrp) rcancel:
+lemma rcancel:
   "y ** x = z ** x <-> y = z"
 proof
   assume "y ** x = z ** x"
   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
     by (simp add: assoc [symmetric])
   then show "y = z" by (simp add: rone rinv)
 qed simp
-*)
-
 
 end
+print_locale! rgrp
+
+end