src/FOL/ex/NewLocaleTest.thy
 changeset 28881 df2525ad10c6 parent 28873 2058a6b0eb20 child 28886 9cb1297b6f13
```--- a/src/FOL/ex/NewLocaleTest.thy	Mon Nov 24 18:04:21 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Nov 24 18:05:20 2008 +0100
@@ -25,7 +25,7 @@
locale param1 = fixes p
print_locale! param1

-locale param2 = fixes p :: 'a
+locale param2 = fixes p :: 'b
print_locale! param2

(*
@@ -54,7 +54,7 @@
print_locale! constraint2

-text {* Groups *}
+text {* Inheritance *}

locale semi =
fixes prod (infixl "**" 65)
@@ -91,7 +91,7 @@
print_locale! pert_hom' thm pert_hom'_def

-text {* Logic *}
+text {* Syntax declarations *}

locale logic =
fixes land (infixl "&&" 55)
@@ -109,7 +109,9 @@
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
@@ -117,15 +119,16 @@
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"
@@ -133,7 +136,8 @@