From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 8 Feb 2006 15:35:08 +0000 (+0000)
Subject: comment out an incomplete proof
X-Git-Tag: make_still_working~7590
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=43d3607afd27248d8df1bca20908307330a3871a;p=helm.git

comment out an incomplete proof
---

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index ed1caebe3..970a5e388 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -244,6 +244,7 @@ for @{ 'disjoint $a $b }.
 interpretation "Left cosets disjoint" 'disjoint C C' =
  (cic:/matita/algebra/groups/left_coset_disjoint.con _ C C').
 
+(*
 (* The following should be a one-shot alias! *)
 alias symbol "belongs_to" (instance 0) = "Belongs to subgroup".
 theorem foo:
@@ -267,6 +268,7 @@ exists;
 | 
 ].
 qed.
+*)
 
 (*theorem foo:
  \forall G:Group. \forall x1,x2:G. \forall H:subgroup G.
@@ -304,4 +306,4 @@ definition left_coset_eq ≝
     (element ? H)·(embed ? ? (subgroup_is_subgroup ? H) ˜ x) =
     (element ? H')·(embed ? ? (subgroup_is_subgroup ? H') ˜ y)).
 *)
-*)
\ No newline at end of file
+*)