--- a/src/HOL/ex/Classpackage.thy Mon Aug 14 13:46:16 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy Mon Aug 14 13:46:17 2006 +0200
@@ -211,18 +211,12 @@
with cancel show ?thesis ..
qed
-interpretation group < monoid
+instance group < monoid
proof -
- fix x :: "'a"
+ fix x
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
qed
-instance group < monoid
-proof
- fix x :: "'a\<Colon>group"
- from group.neutr show "x \<otimes> \<one> = x" .
-qed
-
lemma (in group) all_inv [intro]:
"(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
unfolding units_def
@@ -305,12 +299,17 @@
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
definition
- "x = ((2\<Colon>nat) \<otimes> \<one> \<otimes> 3, (2\<Colon>int) \<otimes> \<one> \<otimes> \<div> 3, [1\<Colon>nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
- "y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
+ "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
+ "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
+
+definition
+ "x1 = X (1::nat) 2 3"
+ "x2 = X (1::int) 2 3"
+ "y2 = Y (1::int) 2 3"
code_generate "op \<otimes>" \<one> inv
-code_generate (ml, haskell) x
-code_generate (ml, haskell) y
+code_generate (ml, haskell) X Y
+code_generate (ml, haskell) x1 x2 y2
code_serialize ml (-)