# 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>\<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 (-)
 
diff -r 39964c8dcd54 -r 58f65fc90cf4 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Aug 14 13:46:16 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Aug 14 13:46:17 2006 +0200
@@ -85,24 +85,24 @@
   h :: nat
   "h = g"
 
-code_alias
-  "Codegenerator.f" "Mymod.f"
-  "Codegenerator.g" "Mymod.A.f"
-  "Codegenerator.h" "Mymod.A.B.f"
+code_constname
+  f "Mymod.f"
+  g "Mymod.A.f"
+  h "Mymod.A.B.f"
 
 code_generate (ml, haskell)
   n one "0::int" "0::nat" "1::int" "1::nat"
 code_generate (ml, haskell)
   fac
-code_generate (ml, haskell)
+code_generate
   xor
-code_generate (ml, haskell)
+code_generate
   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
-code_generate (ml, haskell)
+code_generate
   Pair fst snd Let split swap swapp appl
 code_generate (ml, haskell)
   k
@@ -114,13 +114,13 @@
   fac
   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
-code_generate (ml, haskell)
+code_generate
   Inl Inr
-code_generate (ml, haskell)
+code_generate
   None Some
-code_generate (ml, haskell)
+code_generate
   hd tl "op @" ps qs
-code_generate (ml, haskell)
+code_generate
   mut1 mut2
 code_generate (ml, haskell)
   "op @" filter concat foldl foldr hd tl
@@ -143,7 +143,7 @@
   rotate1
   rotate
   splice
-code_generate (ml, haskell)
+code_generate
   foo1 foo3
 code_generate (ml, haskell)
   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
@@ -153,9 +153,10 @@
   "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+  "op = :: point \<Rightarrow> point \<Rightarrow> bool"
   "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
-code_generate (ml, haskell)
+code_generate
   f g h
 
 code_serialize ml (-)