# HG changeset patch
# User haftmann
# Date 1169713962 -3600
# Node ID 1a3575de2afc50086d5ebc87e77939897c0d4371
# Parent  29b95968272b68e1441c092b6fa2ff83bf00ca05
adjusted to changes in class package

diff -r 29b95968272b -r 1a3575de2afc src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Thu Jan 25 09:32:37 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy	Thu Jan 25 09:32:42 2007 +0100
@@ -220,7 +220,7 @@
 qed
 
 instance group < monoid
-proof -
+proof unfold_locales
   fix x
   from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
 qed
@@ -299,24 +299,24 @@
 instance * :: (semigroup, semigroup) semigroup
   mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
               (x1 \<otimes> y1, x2 \<otimes> y2)"
-by default (simp_all add: split_paired_all mult_prod_def assoc)
+by default (simp_all add: split_paired_all mult_prod_def semigroup_class.assoc)
 
 instance * :: (monoidl, monoidl) monoidl
   one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoidl_class.neutl)
 
 instance * :: (monoid, monoid) monoid
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.neutr)
 
 instance * :: (monoid_comm, monoid_comm) monoid_comm
-by default (simp_all add: split_paired_all mult_prod_def comm)
+by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
 
 instance * :: (group, group) group
   inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def group_class.invl)
 
 instance * :: (group_comm, group_comm) group_comm
-by default (simp_all add: split_paired_all mult_prod_def comm)
+by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
 
 definition
   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
diff -r 29b95968272b -r 1a3575de2afc src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Thu Jan 25 09:32:37 2007 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Thu Jan 25 09:32:42 2007 +0100
@@ -77,7 +77,7 @@
   "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
   by (induct xs) auto
 
-class fin =
+class finite =
   fixes fin :: "'a list"
   assumes member_fin: "x \<in> set fin"
 begin
@@ -96,11 +96,11 @@
 
 end
   
-instance bool :: fin
+instance bool :: finite
   "fin == [False, True]"
   by default (simp_all add: fin_bool_def)
 
-instance unit :: fin
+instance unit :: finite
   "fin == [()]"
   by default (simp_all add: fin_unit_def)
 
@@ -132,24 +132,24 @@
   qed
 qed
 
-instance * :: (fin, fin) fin
+instance * :: (finite, finite) finite
   "fin == product fin fin"
 apply default
 apply (simp_all add: "fin_*_def")
 apply (unfold split_paired_all)
 apply (rule product_all)
-apply (rule member_fin)+
+apply (rule finite_class.member_fin)+
 done
 
-instance option :: (fin) fin
+instance option :: (finite) finite
   "fin == None # map Some fin"
 proof (default, unfold fin_option_def)
-  fix x :: "'a::fin option"
+  fix x :: "'a::finite option"
   show "x \<in> set (None # map Some fin)"
   proof (cases x)
     case None then show ?thesis by auto
   next
-    case (Some x) then show ?thesis by (auto intro: member_fin)
+    case (Some x) then show ?thesis by (auto intro: finite_class.member_fin)
   qed
 qed
 
@@ -193,9 +193,6 @@
 (*definition "test2 = (inf :: nat \<times> unit)"*)
 definition "test3 \<longleftrightarrow> (\<exists>x \<Colon> bool option. case x of Some P \<Rightarrow> P | None \<Rightarrow> False)"
 
-code_gen test3
-
-code_gen (SML #)
-code_gen (Haskell -)
+code_gen test3 (SML #) (OCaml -) (Haskell -)
 
 end
\ No newline at end of file