instantiation replacing primitive instance plus overloaded defs

--- a/src/HOL/Bali/Decl.thy	Mon Apr 07 15:37:32 2008 +0200
+++ b/src/HOL/Bali/Decl.thy	Mon Apr 07 15:37:33 2008 +0200
@@ -6,7 +6,9 @@
 *}
 
 (** order is significant, because of clash for "var" **)
-theory Decl imports Term Table begin
+theory Decl
+imports Term Table
+begin
 
 text {*
 improvements:
@@ -50,21 +52,21 @@
   Private < Package < Protected < Public
 *}
  
-instance acc_modi:: ord ..
+instantiation acc_modi :: linorder
+begin
 
-defs (overloaded)
-less_acc_def: 
- "a < (b::acc_modi) 
-      \<equiv> (case a of
+definition
+  less_acc_def: "a < b
+      \<longleftrightarrow> (case a of
              Private    \<Rightarrow> (b=Package \<or> b=Protected \<or> b=Public)
            | Package    \<Rightarrow> (b=Protected \<or> b=Public)
            | Protected  \<Rightarrow> (b=Public)
            | Public     \<Rightarrow> False)"
-le_acc_def:
- "a \<le> (b::acc_modi) \<equiv> (a = b) \<or> (a < b)"
 
-instance acc_modi:: order
-proof
+definition
+  le_acc_def: "a \<le> (b::acc_modi) \<longleftrightarrow> (a = b) \<or> (a < b)"
+
+instance proof
   fix x y z::acc_modi
   {
   show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
@@ -86,14 +88,12 @@
   show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
     by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
   }
-qed
-  
-instance acc_modi:: linorder
-proof
   fix x y:: acc_modi
   show  "x \<le> y \<or> y \<le> x"   
   by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
 qed
+  
+end
 
 lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public"
 by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

--- a/src/HOL/Hyperreal/HyperDef.thy	Mon Apr 07 15:37:32 2008 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Apr 07 15:37:33 2008 +0200
@@ -43,11 +43,16 @@
 
 subsection {* Real vector class instances *}
 
-instance star :: (scaleR) scaleR ..
+instantiation star :: (scaleR) scaleR
+begin
 
-defs (overloaded)
+definition
   star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
 
+instance ..
+
+end
+
 lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
 by (simp add: star_scaleR_def)