diff -r a6e26a248f03 -r 7ab2716dd93b src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/UNITY/Comp.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -15,14 +15,22 @@
 
 header{*Composition: Basic Primitives*}
 
-theory Comp imports Union begin
+theory Comp
+imports Union
+begin
 
-instance program :: (type) ord ..
+instantiation program :: (type) ord
+begin
 
-defs
-  component_def:          "F \<le> H == \<exists>G. F\<squnion>G = H"
-  strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
+definition
+  component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
 
+definition
+  strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
+
+instance ..
+
+end
 
 constdefs
   component_of :: "'a program =>'a program=> bool"
@@ -114,7 +122,7 @@
 by (auto simp add: stable_def component_constrains)
 
 (*Used in Guar.thy to show that programs are partially ordered*)
-lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
+lemmas program_less_le = strict_component_def
 
 
 subsection{*The preserves property*}
@@ -229,8 +237,7 @@
 apply (blast intro: Join_assoc [symmetric])
 done
 
-lemmas strict_component_of_eq =
-    strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
+lemmas strict_component_of_eq = strict_component_of_def
 
 (** localize **)
 lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"