# HG changeset patch
# User wenzelm
# Date 1005153436 -3600
# Node ID 08b4da78d1adc723f32dab6bdb1b58b9df980435
# Parent  e70c7350851c5210ef25dad39e372b424b38e986
added structures;
tuned;

diff -r e70c7350851c -r 08b4da78d1ad src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Wed Nov 07 18:16:54 2001 +0100
+++ b/src/HOL/ex/Locales.thy	Wed Nov 07 18:17:16 2001 +0100
@@ -4,22 +4,22 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Locales and simple mathematical structures *}
+header {* Basic use of locales *}
 
 theory Locales = Main:
 
+text {*
+  The inevitable group theory examples formulated with locales.
+*}
+
+
+subsection {* Local contexts as mathematical structures *}
+
 text_raw {*
   \newcommand{\isasyminv}{\isasyminverse}
   \newcommand{\isasymone}{\isamath{1}}
 *}
 
-
-subsection {* Groups *}
-
-text {*
-  Locales version of the inevitable group example.
-*}
-
 locale group =
   fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
     and inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
@@ -119,4 +119,37 @@
   finally show ?thesis .
 qed
 
-end
+
+subsection {* Referencing structures implicitly *}
+
+record 'a semigroup =
+  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+syntax
+  "_prod1" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
+  "_prod2" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>\<^sub>2" 70)
+  "_prod3" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>\<^sub>3" 70)
+translations
+  "x \<odot> y" \<rightleftharpoons> "(\<struct>prod) x y"
+  "x \<odot>\<^sub>2 y" \<rightleftharpoons> "(\<struct>\<struct>prod) x y"
+  "x \<odot>\<^sub>3 y" \<rightleftharpoons> "(\<struct>\<struct>\<struct>prod) x y"
+
+lemma
+  (fixes S :: "'a semigroup" (structure)
+    and T :: "'a semigroup" (structure)
+    and U :: "'a semigroup" (structure))
+  "prod S a b = a \<odot> b" ..
+
+lemma
+  (fixes S :: "'a semigroup" (structure)
+    and T :: "'a semigroup" (structure)
+    and U :: "'a semigroup" (structure))
+  "prod T a b = a \<odot>\<^sub>2 b" ..
+
+lemma
+  (fixes S :: "'a semigroup" (structure)
+    and T :: "'a semigroup" (structure)
+    and U :: "'a semigroup" (structure))
+  "prod U a b = a \<odot>\<^sub>3 b" ..
+
+end
\ No newline at end of file