--- 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*}