diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/UNITY/Guar.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -18,13 +18,12 @@
 
 header{*Guarantees Specifications*}
 
-theory Guar imports Comp begin
+theory Guar
+imports Comp
+begin
 
 instance program :: (type) order
-  by (intro_classes,
-      (assumption | rule component_refl component_trans component_antisym
-                     program_less_le)+)
-
+proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
 
 text{*Existential and Universal properties.  I formalize the two-program
       case, proving equivalence with Chandy and Sanders's n-ary definitions*}