# HG changeset patch # User haftmann # Date 1155555977 -7200 # Node ID 58f65fc90cf403f8de672591a76b69eb530bbfe6 # Parent 39964c8dcd54d515d6d766c4e5b559cfee2a0d5a adaptions to improvements diff -r 39964c8dcd54 -r 58f65fc90cf4 src/HOL/ex/Classpackage.thy --- 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>\ \<^loc>\ = x" . qed -instance group < monoid -proof - fix x :: "'a\group" - from group.neutr show "x \ \ = x" . -qed - lemma (in group) all_inv [intro]: "(x\'a) \ monoid.units (op \<^loc>\) \<^loc>\" 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\nat) \ \ \ 3, (2\int) \ \ \ \
3, [1\nat, 2] \ \ \ [1, 2, 3])" - "y = (2 \ int, \
2 \ int) \ \ \ (3, \
3)" + "X a b c = (a \ \ \ b, a \ \ \ b, [a, b] \ \ \ [a, b, c])" + "Y a b c = (a, \
a) \ \ \ \
(b, \