From 43d3607afd27248d8df1bca20908307330a3871a Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 8 Feb 2006 15:35:08 +0000
Subject: [PATCH] comment out an incomplete proof
---
helm/software/matita/library/algebra/groups.ma | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
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
+*)
--
2.39.2